Invited Papers
Model Checking Algorithms for Hyperproperties
Algebra-based Synthesis of Loops and their Invariants
Generative Program Analysis and Beyond: The Power of Domain-Specific Languages
Hyperproperties and Infinite-state Systems
Compositional Model Checking for Multi-Properties
Decomposing Data Structure Commutativity Proofs with mn-Differencing
Proving the existence of fair paths in infinite-state systems
A Self-Certifying Compilation Framework for WebAssembly
Concurrent and Distributed Systems
Concurrent Correctness in Vector Space
Verification of Concurrent Programs Using Petri Net Unfoldings
Eliminating Message Counters in Synchronous Threshold Automata
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
Checking
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
Twinning automata and regular expressions for string static analysis
Unbounded Procedure Summaries from Bounded Environments
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
Synthesis and Repair
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
GPURepair: Automated Repair of GPU Kernels
Applications
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
A Design of GPU-Based Quantitative Model Checking
Formal Semantics and Verification of Network Based Biocomputation Circuits
Netter: Probabilistic, Stateful Network Models, . Decision Procedures
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
On Preprocessing for Weighted MaxSAT
Compositional Satisfiability Solving in Separation Logic.