Verifying Arithmetic Circuits with Polynomials (abstract)

Software Verification Witnesses (abstract)

Witness-guided verification in trace abstraction (abstract)

From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification (abstract)

Arithmetic Solving in Z3 (abstract)

First-Order Proof Checking (abstract)

Proof-based Space Explanation of Classifying Neural Networks (abstract)

On the Verification of Structured Parameterized Networks (abstract)

Hardware-Optimal Quantum Algorithms (abstract)

Bounding Probabilistic Loop Variables using Martingales and the Optional Stopping Theorem (abstract)

Formal Verification with Configurable Execution Semantics (abstract)

Computing abstract model-checking transitions using abstract interpretation (abstract)

Parameterized Infinite-State Reactive Synthesis (abstract)

Neural Certificates (abstract)

Regexes with Back-References using Register Set Automata (abstract)

Towards Minimizing Phase Event Automata (abstract)

Complementing Emerson-Lei Elevator Automata (abstract)

Leveraging Partial Redundancy in Active Automata Learning (abstract)

Accelerating Decision-diagram-based Quantum Circuit Simulation With Symbolic Execution (abstract)

A Novel Symbolic Execution Framework for Symbolic Timing Analysis of Digital Integrated Circuits (abstract)

RacerF: Lightweight Static Data Race Detection for C Code (abstract)

CHCs for every occasion (abstract)

Current State of String Solver Z3-Noodler (abstract)

On User-defined Decision Guidance in SMT Solvers (abstract)

Pseudo-Boolean Proof Logging for Optimal Classical Planning (abstract)

Proofs (that contain programs that contain proofs)* (abstract)

Robust by Design: SAT-based Automata Learning in the Presence of Noise (abstract)