This book constitutes the proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021, which was held virtually during January 17-19, 2021. The conference was planned to take place in Copenhagen, Denmark, but changed to an online event due to the COVID-19 pandemic.
The 23 papers presented in this volume were carefully reviewed from 48 submissions. VMCAI provides a forum for researchers working on verification, model checking, and abstract interpretation and facilitates interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. The papers presented in this volume were organized in the following topical sections: hyperproperties and infinite-state systems; concurrent and distributed systems; checking; synthesis and repair; applications; and decision procedures.
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.
