Theorem Proving
Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning
Efficient verification of imperative programs using auto2
Frame Inference for Inductive Entailment Proofs in Separation Logic
Verified Model Checking of Timed Automata
SAT and SMT I
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
CDCLSym: Introducing E_ective Symmetry Breaking in SAT Solving
Automatic Generation of Precise and Useful Commutativity Conditions
Bit-Vector Model Counting using Statistical Estimation
Deductive Verification
Hoare Logics for Time Bounds
A Verified Implementation of the Bounded List Container
Automating Deductive Verification for Weak-Memory Programs
Software Verification and Optimisation
Property Checking Array Programs Using Loop Shrinking
Invariant Synthesis for Incomplete Verification Engines
Accelerating Syntax-Guided Invariant Synthesis
Daisy
Framework for Analysis and Optimization of Numerical Programs
Model Checking
Oink: an Implementation and Evaluation of Modern Parity Game Solvers
More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D^3)
Generation of Minimum Tree-like Witnesses for Existential CTL
From Natural Projection to Partial Model Checking and Back
Machine Learning
ICE-based Refinement Type Discovery for Higher-Order Functional Programs
Strategy Representation by Decision Trees in Reactive Synthesis
Feature-Guided Black-Box Safety Testing of Deep Neural Networks. .