ABSTRACT. Formal verification of arithmetic circuits remains a challenging problem at the intersection of SAT solving, SMT, and computer algebra. While SAT-based techniques have achieved remarkable success across many verification domains, arithmetic hardware continues to pose significant challenges. One of the most effective approaches in this setting relies on algebraic reasoning: a circuit, represented as an and-inverter graph, is encoded as a system of polynomials that induces a Gröbner basis, and correctness is established by reducing a polynomial specification with respect to this basis. In the first part of this talk, I will provide an overview of arithmetic circuit verification and discuss how SAT solving and computer algebra can be combined to discover structural information and enabling simplifications that are difficult to obtain through purely algebraic methods. In the second part, I will present a recent approach that addresses one of the main bottlenecks of algebraic verification: the monomial blow-up that occurs during specification rewriting. Rather than focusing computational effort on rewriting the specification, we rewrite the Gröbner basis itself to expose useful linear relations using algebraic guesses and SAT-based proofs. The resulting approach significantly simplifies the reduction process and improves the scalability of arithmetic circuit verification.

ABSTRACT. We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging. A reduction-based decision procedure for the theory is given. Finally, we describe an implementation of the procedure, as well as an evaluation over both real-world and crafted benchmarks.

ABSTRACT. The Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear integer and real arithmetic. In this paper we revisit the theory-independent MCSat framework as a proof system to provide a modern perspective that refines the original formulation of MCSat. By closely formalizing the implementation of MCSat within the Yices2 SMT solver, we incorporate design decisions that diverge from those in the seminal MCSat paper and thereby capture the current state-of-the-art in MCSat-based SMT reasoning. We present a general, theory-agnostic rule scheme for MCSat and instantiate it for several theories, including propositional logic, non-linear real arithmetic, and uninterpreted functions. We provide several detailed examples to illustrate the applicability of the presented calculus.

ABSTRACT. We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and trigonometric ones. The framework extends the Model Constructive Satisfiability calculus (MCSAT), and leverages procedures for NRA and methods from real analysis. At its core, our procedure abstracts the input formula to NRA, and lets MCSAT and an NRA plugin incrementally builds a partial model of the abstracted formula. A Transcendental Real Arithmetic plugin, acting as an intermediary between MCSAT and the NRA plugin, ensures the consistency of the partial model and is responsible for refining the abstracted formula. We implemented our procedure in the Yices2 SMT solver for the sine and exponential functions, and conducted an extensive empirical evaluation that shows that our implementation outperforms state-of-the-art solvers on both SAT and UNSAT instances.

ABSTRACT. Satisfiability modulo non-linear real arithmetic is about checking Boolean combinations of polynomial constraints. The non-uniform CAD (NuCAD) and cylindrical algebraic covering (CAlC) algorithms are variants of the complete cylindrical algebraic decomposition (CAD) algorithm which reduce effort by transferring the exploration-guided technique from SAT solving, so that the trace of these algorithms can be described as a search tree. The modification in this paper alters the order in which the search tree is explored, deferring the exploration of branches with expensive computations to potentially find an easier-to-compute solution. We adapt both the NuCAD and CAlC algorithms. In the experimental evaluation, NuCAD solves a significant number of previously unsolved instances, whereas CAlC does not benefit from the modification.

ABSTRACT. We address the satisfiability problem for quantified nonlinear integer arithmetic (NIA), which is undecidable even in the quantifier-free case. Our approach reduces NIA formulas to linear integer arithmetic (LIA) by replacing nonlinear terms with fresh existential variables---a process we call purification. The resulting LIA abstraction over-approximates the original problem and is iteratively refined by adding axioms that constrain the abstracted terms to respect their nonlinear semantics. Experimental evaluation on SMT-LIB benchmarks and randomly generated polynomial representation problems outperforms state-of-the-art solvers. In the case of representation problems, our prototype solves more than twice as many instances as the next-best solver (yicesQS).

ABSTRACT. Formal verification of cryptographic protocols in the computational model provides strong security guarantees but remains challenging to automate. The Computationally Complete Symbolic Attacker (CCSA) logic, implemented in the Squirrel proof assistant, provides computationally sound reasoning in a polymorphic higher-order logic whose validity is defined as overwhelming truth. Recently, we introduced an SMT-based tactic to automate a first-order fragment of that logic, but higher-order constructs and polymorphism were left unsupported. In this paper, we extend our approach to automate the full local logic of Squirrel. We implement this translation in Squirrel's SMT tactic and demonstrate its effectiveness on generic benchmarks and several case studies.

ABSTRACT. We introduce a dependently typed theory of floating-point arithmetic for SMT-LIB 3 in which exponent and significand widths are symbolic parameters. This enables reasoning about format-parametric properties that cannot be expressed in SMT-LIB 2. We implement MC-Hammer, an extension of Isabelle/HOL's Sledgehammer, which translates polymorphic floating-point terms into SMT-LIB 3 with dependent types. Using this infrastructure, we generate over 600 benchmark problems covering both fixed and symbolic sizes. Our work provides the first practical bridge between interactive theorem provers and SMT-LIB 3 for floating-point reasoning.

ABSTRACT. Whether LLMs can reason or write software is widely debated, but whether they can write software that itself reasons is largely unexplored. We present a case study in which an LLM coding agent builds a complete DPLL(T)-style SMT solver for QF_UF with zero human-written code. The solver implements the Nieuwenhuis-Oliveras congruence closure algorithm, includes preprocessing, and emits Lean proofs for unsatisfiable instances. We describe the development process and key challenges, and show that the resulting solver is competitive on SMT-LIB benchmarks. While full proof emission for unsatisfiable instances appears to be beyond the capabilities of the LLM, the solver achieves competitive performance and passes correctness tests.

ABSTRACT. Algorithm selection is important in satisfiability and constraint solving, since no single solver performs best across all instances. Traditional learning-based approaches represent problem instances using expert-designed features to predict solver performance, while recent work explores graph representations derived from ASTs. However, most existing approaches overlook high-level contextual information, such as the application domain or the benchmark origin. In practice, such cues often help practitioners choose an appropriate solver. We present SMT-Select, a multimodal framework for SMT algorithm selection. It learns graph representations from formula ASTs and textual representations from natural-language context descriptions. These representations are then combined to guide solver selection. Evaluated across nine SMT logics, SMT-Select consistently outperforms existing selectors and SMT-COMP winning solvers. Across all evaluated logics, it closes at least 30% of the performance gap between the competition winner and the virtual best solver (VBS), and nearly matches the VBS in two logics.

ABSTRACT. Satisfiability Modulo Theory (SMT) has recently emerged as a powerful tool for solving various automated reasoning problems across diverse domains. Unlike traditional satisfiability methods confined to Boolean variables, SMT can reason on real-life variables like bitvectors, integers, and reals. A natural extension in this context is to ask quantitative questions. One such query in the SMT theory of Linear Real Arithmetic (LRA) is computing the volume of the entire satisfiable region defined by SMT formulas. This problem is important in solving different quantitative verification queries in software verification, cyber-physical systems, and neural networks, to mention a few. We introduce ttc, an efficient algorithm that extends the capabilities of SMT solvers to volume computation. Our method decomposes the solution space of SMT Linear Real Arithmetic formulas into a union of overlapping convex polytopes, then computes their volumes and calculates their union. Our algorithm builds on recent developments in streaming-mode set unions, volume computation algorithms, and AllSAT techniques. Experimental evaluations demonstrate significant performance improvements over existing state-of-the-art approaches.