Invited Papers
NNrepair: Constraint-based Repair of Neural Network Classifiers
Balancing automation and control for formal verification of microprocessors
Algebraic Program Analysis
Programmable Program Synthesis
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities
AI Verification
DNNV: A Framework for Deep Neural Network Verification
Robustness Verification of Quantum Classifiers
BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
Automated Safety Verification of Programs Invoking Neural Networks
Scalable Polyhedral Verification of Recurrent Neural Networks
Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning
Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability
PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier
Concurrency and Blockchain
Isla: Integrating full-scale ISA semantics and axiomatic concurrency models
Summing Up Smart Transitions
Stateless Model Checking under a Reads-Value-From Equivalence
Gobra: Modular Specification and Verification of Go Programs
Delay-Bounded Scheduling Without Delay!
Checking Data-Race Freedom of GPU Kernels, Compositionally
GenMC: A Model Checker for Weak Memory Models
Hybrid and Cyber-Physical Systems
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation
HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL
Computing Bottom SCCs Symbolically Using Transition Guided Reduction
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems
IMITATOR 3: Synthesis of timing parameters beyond decidability
Formally Verified Switching Logic for Recoverability of Aircraft Controller
SceneChecker: Boosting Scenario Verification using Symmetry Abstractions
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
Fast zone-based algorithms for reachability in pushdown timed automata
Security
Verified Cryptographic Code for Everybody
Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference
A Temporal Logic for Asynchronous Hyperproperties
Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security
Constraint-based Relational Verification
Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning
Synthesis
Synthesis with Asymptotic Resource Bounds
Program Sketching by Automatically Generating Mocks from Tests
Counterexample-Guided Partial Bounding for Recursive Function Synthesis
PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs
Adapting Behaviors via Reactive Synthesis
Causality-based Game Solving.