ABSTRACT. Formal verification using computer algebra has emerged as a powerful approach for circuit verification. This technique encodes a circuit, represented as an and-inverter graph, into a set of polynomials that generates a Gröbner basis. Verification relies on computing the polynomial remainder of the specification. But there is a catch: a monomial blow-up often occurs during specification rewriting — a problem that often necessitates dedicated heuristics to manage the complexity. In the first part of the talk, I will provide an introduction to arithmetic circuit verification and discuss how computer algebra can be used in this setting. In the second part, I will present a novel approach, which shifts the computational effort to rewriting the Gröbner basis itself rather than the specification. By restructuring the basis to include linear polynomials, we tame the monomial blow-up and simplify the rewriting process.

ABSTRACT. Software verification witnesses are a concept which has emerged in the last decade to aid in tool interoperability and user interaction. Software verification witnesses are a machine-readable data format that allows tools to encode information about their verification process as invariants for correctness arguments or paths through a program leading to an error. In this talk, I will provide an introduction to software verification witnesses, focusing on the recent developments in tool interoperability, format extensions and cooperative verification.

ABSTRACT. Witnesses are a standardized exchange format between software verification tools, enabling reuse of verification results. While witnesses can be validated - and many validators exist - validating correctness witnesses is often slower than performing verification without a witness. If the goal is solely to verify the program, the information from a witness can instead be used as hints to accelerate verification, without validating the witness. We refer to this approach as witness-guided verification. In this talk, we demonstrate how witness-guided verification for correctness witnesses can be integrated into the trace abstraction algorithm to accelerate verification.

ABSTRACT. Implementation bugs in software verifiers can undermine their results. Generating correctness certificates enables efficient, independent validation, helping to expose such flaws. For concurrent programs, however, proofs often depend on specific thread interleavings, leading to exponential blow-ups. In this talk, we present a method that uses Empires, a compact intermediate representation, to transform interleaving-based proofs into concise, thread-modular proofs in the Owicki–Gries style. Owicki–Gries proofs are a thread-modular reasoning technique for concurrent programs that ensures inductivity and interference freedom between threads, with ghost variables recording relevant interleaving information needed for the proof. Our approach automatically synthesizes ghost variables to capture only the relevant interleaving information, abstracting away the rest.

ABSTRACT. The tutorial describes solvers for arithmetic in z3. Arithmetic formulas of interest for SMT users range from Pseudo-Boolean to non-linear integer arithmetic and beyond. They are used for checking satisfiability of quantifier-free and quantified formulas, for synthesizing solutions to Constrained Horn Clauses and for optimization objectives. The solvers integrate pre-processing, techniques from mixed integer linear programming, Grobner bases, Cylindric Algebraic Decomposition, incremental linearization, and local search. We provide an architectural overview of the arithmetic solvers and internals of selected sub-solvers and outline several directions.

ABSTRACT. Saturation-based first-order theorem provers are becoming increasingly sophisticated, especially when they are used for reasoning with both quantifiers and theories, such as arithmetic. This makes proof-checking important, complex and challenging.

In essence, the proof-checking problem is the problem that consists of two parts:

1. producing proofs which are detailed enough so that they consist of steps which could be checked for correctness, preferably using algorithms with low complexity (checkable proofs);
2. implementing tools that check the correctness of such proofs

There has been a considerable interest in proof-checking of SAT and SMT solvers. Our focus is on first-order proofs. While first-order provers, such as Vampire, produce proofs, they are far from being checkable.

We will discuss 

1. what is proof-checking
2. problems with first-order proof checking
3. existing solutions
4. an example: ground truth proof checking (by Anja Petković Komel, Michael Rawson, Johannes Schoisswohl and Andrei Voronkov)

Many concepts and problems discussed in the talk are relevant to higher-order theorem proving and theorem proving in type theories as used by modern proof assistants.

ABSTRACT. We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by state-of-the-art.

ABSTRACT. We consider the verification of parameterized networks with architectures specified by graph grammars in the style of Courcelle's Hyperedge- and Vertex-Replacement grammars. The networks are made of replicated processes that communicate via pairwise rendezvous according to the network's parameterized communication topology.

To bypass the undecidability of the problem in general, we develop and prototype an abstraction technique that provides a semi-algorithm, and we identify decidable restrictions.

This talk will contain elements from - Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks, published at CAV'25 - Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars, published at NETYS'25 - ongoing work

ABSTRACT. Quantum hardware is inherently fragile and noisy. We find that the accuracy of traditional quantum error correction algorithms can be improved depending on the hardware. Given different hardware specifications, we automatically synthesize hardware-optimal algorithms for parity correction, qubit resetting, and GHZ state preparation. Using stochastic techniques from computer science, our method presents a new computational tool to compute exact accuracy guarantees and synthesize optimal algorithms that are often different from traditional ones. We also show that improvements can be gained with respect to the Qiskit transpiler as we compute the hardware-optimal qubit mapping for the GHZ state-preparation problem.

ABSTRACT. For probabilistic programs, a Martingale is an expression for which the conditional expected value at the next state is equal to its current value, given its current and past values. For such Programs, Martingales serve as invariants, but in contrast to their deterministic counterpart they do not necessarily hold at the end of the loop. In this talk, I will present ongoing research about how to use Martingales to compute symbolic bounds for loop variables at the end of the loop, by utilizing a version of the Optional Stopping Theorem.