In deductive verification, a verifying compiler generates verification conditions (VCs) for an annotated program. The VCs are submitted to an automated reasoner: if they are valid, the proofs certify the verification. Otherwise, counter-models represented by assignments offer guidance for debugging. Since first-order logic is only semidecidable, the VCs ought to be written in decidable fragments. Since the VCs involve symbols defined by more than one first-order theory, the automated reasoner should handle efficiently decidable theory combinations, producing proofs and models. The model-based conflict-driven style of the CDCL procedure is deemed efficient in propositional logic (PL). CDSAT brings this style to theory combination. Unlike Nelson-Oppen, which combines theories by combining procedures, CDSAT reasons directly in the theory union, by coordinating theory inference systems, called theory modules. Unlike CDCL(T), the conflict-driven reasoning happens in the theory union, not only in PL, which is one of the theories for CDSAT. CDSAT encompasses CDCL, Nelson-Oppen, CDCL(T), and MCSAT, as CDSAT was inspired by the idea of generalizing the MCSAT calculus to the multi-theory setting. The flexibility of CDSAT is demonstrated by showing how it allows us to reason in new theories of arrays, maps, and vectors (i.e., dynamic arrays) with abstract domain, that overcome the limitations of the standard theory or arrays. The session presents first CDSAT and then its application to reasoning about these data structures.

In this course, we will focus on sequential SAT solving techniques and how to interact with it from a user perspective. We will first describe the main components of conflict-driven clause learning (CDCL) architecture used in most SAT solvers, invented around 30 years ago.

However, there is reasoning that goes beyond CDCL (like the discovery of equivalent literals). These techniques complement CDCL and have been the main change in SAT solvers in the last 15 years. They are now needed to win the SAT Competition.

SAT Solver are large pieces code (CaDiCaL is more than 60k lines of C++) and their correctness is very important. Hence, independant proof checkers and proof formats have been developped both for SAT solving and for incremental SAT solving in recent years.

Finally the most recent changes are the better interaction with users, via user propagators. They make it possible for users to slowly give clauses to SAT solvers, potentially avoiding the exponential blow-up that can happen during the encoding.

Satisfiability Modulo Theories (SMT) solvers have become indispensable tools for hardware design, software verification, and security analysis by extending propositional logic with rich domain-specific theories. While ground formulas are handled reliably via the robust DPLL(T) architecture, the inclusion of first-order quantifiers introduces inherent undecidability, forcing solvers to rely on a complex portfolio of hand-crafted heuristics to find relevant ground instances. Traditionally, these heuristics are rigid and difficult to tune. This lecture explores the general landscape of SMT solving and evaluates the strategic opportunities for integrating machine learning into this deterministic world. Rather than replacing the core solver, modern neural approaches excel at learning data-driven heuristics—such as guiding quantifier selection and term generation—directly from past solving attempts. However, blending exact logical reasoning with approximate machine learning presents a dual challenge: avoiding the massive computational overhead of deep neural network evaluation at inference time, and maintaining absolute soundness. The lecture will highlight these practical tradeoffs, review recent milestones in neural-guided SMT, and discuss the open frontier of self-contained, data-driven automated reasoning.

In this lecture, we will study how analysis methods defined for higher-order term rewriting can be applied to analyse small functional programs, in particular the question of termination. We study this question in an open world: how can we analyse a single module in a larger program, and yet get a meaningful result out of the analysis that is valuable also regarding the program as a whole. If time permits, we will also consider how these termination results can be used to analyse equivalence (e.g.,to answer the question if a function can be replaced by another without altering the functioning of the program).

Arithmetic circuits play a crucial role in many computationally intensive applications today as well as in upcoming AI architectures. In spite of intensive research efforts that have been made during the last years, arithmetic circuits still form a major challenge for automatic verification technologies. A wide range of architectures has been proposed for arithmetic units, which take advantage of sophisticated algorithms to meet different optimization goals and are usually extensively parallel and structurally complex. Thus, it is very difficult to ensure the correctness of such arithmetic circuit implementations.

I will present a fully automatic formal verification methodology based on Symbolic Computer Algebra that goes far beyond incomplete simulation-based approaches and semi-automatic approaches based on theorem proving which are still the state-of-the-art for arithmetic circuit verification at many places in industry. Only *formal* verification is able to provide rigorous correctness guarantees. *Full automation* is needed, since the design of circuits containing arithmetic is nowadays not only confined to the major processor vendors, but is also done by many different suppliers of special-purpose embedded hardware who cannot afford to employ large teams of specialized verification engineers being able to provide human-assisted theorem proofs.

In this talk I will show several improvements to the basic Symbolic Computer Algebra approach to arithmetic circuit verification and I will demonstrate their impact on the verification of multipliers and dividers with large bitwidths.