Large language models have great potential to be pedagogical tools, able to interact with students as a tutor would, answering questions, addressing misunderstandings, using the Socratic method, etc. They can supplement in-person teaching with an availability and scale that cannot be economically provided by instructors and TAs. However, simply directing a generally available chatbot to be a tutor on a specific topic is likely to go down paths that are not relevant or appropriate for a specific class context. We have developed a ''focused tutor'' system in which instructors can create custom, targeted tutors by defining learning objectives and assessment questions. Instructors can deploy multiple tutors in a course, each tailored to a different module or goal in the specific context of that class, and assign them to students as low-stakes assessments following a reading or video. The intent is to provide a step between encountering material outside of class and working with it in class that is more engaging and provides more benefit to the students than a static reading response or reading quiz. In this lightning talk, we will present the motivation, design, and use of this tool, seeking feedback, ideas, and potential collaborations in studying this type of tool.

We begin a systematic study of how Graph Decomposition problems may be represented using propositional formulas, and hence solved using SAT-solver technology. By making use of symmetry breaking techniques we are able to obtain solutions to several previously unknown cases and to significantly reduce the time needed to compute decompositions. However some fairly small instances remain unsolved, and thus provide an interesting challenge to SAT-solver technology.

The problem of enumerating minimal unsatisfiable subsets of a constraint system (MUSes) is a natural candidate for parallelization: as an enumeration problem, it allows for concurrent solving of independent subproblems, and as a typically intractable problem w.r.t. completion (which parallelization cannot transcend), the speed or rate of output (which parallelization can improve) is often the most important performance characteristic. In this work, we explore the parallelization of partial MUS enumeration (aiming to enumerate some MUSes within given resource constraints) via two extensions to a recently-developed sequential algorithm - one employing an existing parallel single-MUS extraction algorithm, the other parallelizing the entire enumeration algorithm-- and we discuss variants and implementation details as well. Results of experiments run with up to 16 cores show that the full parallelization of the entire enumeration algorithm scales well, reaching an average of 92% of perfect scaling with 4 cores and 70% at 16 cores. Evaluating variants and implementation details illuminates how those choices impact performance, including a potentially counterintuitive result that sharing results between threads to avoid duplicate work is not beneficial in the general case.

Static analysis techniques can be used to compute safe bounds on the worst-case execution time (WCET) of programs. For large programs, abstractions are often required to curb computational complexity. These abstractions may introduce infeasible paths which result in significant overestimation. These paths can be eliminated by adding additional constraints to the static analysis. Such constraints can be found manually but this is labour-intensive and error-prone. Automated methods of finding infeasible path constraints are thus highly desirable. In this paper we present Trickle: a method to automatically detect infeasible paths on compiled binary programs, in order to refine WCET estimates. We build upon the Sequoll framework and apply satisfiability modulo theory (SMT) solvers to find classes of infeasible paths. Unlike other techniques, Trickle can find infeasible paths which contain an arbitrary number of conflicting conditions. We also integrate the compute all minimal unsatisfiable subsets (CAMUS) algorithm to reduce the number of refinement iterations required. We show the practicality of Trickle by applying it to a WCET analysis of the seL4 microkernel. We also evaluate its effectiveness on the Mälardalen WCET benchmarks.

In today's SoC design cycles, debugging is one of the most time consuming manual tasks. CAD solutions strive to reduce the inefficiency of debugging by identifying error sources in designs automatically. Unfortunately, the capacity and performance of such automated techniques must be considerably extended for industrial applicability. This work aims to improve the performance of current state-of-the-art debugging techniques, thus making them more practical. More specifically, this work proposes a novel design debugging formulation based on maximum satisfiability (max-sat) and approximate max-sat. The developed technique can quickly discard many potential error sources in designs, thus drastically reducing the size of the problem passed to an existing debugger. The max-sat formulation is used as a pre-processing step to construct a highly optimized debugging framework. Empirical results demonstrate the effectiveness of the proposed framework as run-time improvements of orders of magnitude are consistently realized over a state-of-the-art debugger.

In this paper, we explore the application of counter-example-guided abstraction refinement (CEGAR) in the context of microprocessor correspondence checking. The approach utilizes automatic datapath abstraction augmented with automatic refinement based on 1) localization, 2) generalization, and 3) minimal unsatisfiable subset (MUS) extraction. We introduce several refinement strategies and empirically evaluate their effectiveness on a set of microprocessor benchmarks. The data suggest that localization, generalization, and MUS extraction from both the abstract and concrete models are essential for effective verification. Additionally, refinement tends to converge faster when multiple MUses are extracted in each iteration.

Instances of the Boolean satisfiability problem (SAT) arise in many areas of circuit design and verification. These instances are typically constructed from some human-designed artifact, and thus are likely to possess much inherent symmetry and sparsity. Previous work[4] has shown that exploiting symmetries results in vastly reduced SAT solver run times, often with the search for the symmetries themselves dominating the total SAT solving time. Our contribution is twofold. First, we dissect the algorithms behind the venerable NAUTY[9] package, particularly the partition refinement procedure responsible for the majority of search space pruning as well as the majority of run time overhead. Second, we present a new symmetry-detection tool, SAUCY, which outperforms NAUTY by several orders of magnitude on the large, structured CNF formulas generated from typical EDA problems.