Verification, Model Checking, and Abstract Interpretation

1. Front Matter

   Pages i-xv

   PDF

2. Invited Papers

   1. Front Matter

      Pages 1-1

      PDF

   2. Model Checking Algorithms for Hyperproperties (Invited Paper)

      • Bernd Finkbeiner

      Pages 3-16

   3. Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)

      • Andreas Humenberger, Laura Kovács

      Pages 17-28

   4. Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper)

      • Bernhard Steffen, Alnis Murtovi

      Pages 29-51

3. Hyperproperties and Infinite-State Systems

   1. Front Matter

      Pages 53-53

      PDF

   2. Compositional Model Checking for Multi-properties

      • Ohad Goudsmid, Orna Grumberg, Sarai Sheinvald

      Pages 55-80

   3. Decomposing Data Structure Commutativity Proofs with \(m\!n\)-Differencing

      • Eric Koskinen, Kshitij Bansal

      Pages 81-103

   4. Proving the Existence of Fair Paths in Infinite-State Systems

      • Alessandro Cimatti, Alberto Griggio, Enrico Magnago

      Pages 104-126

   5. A Self-certifying Compilation Framework for WebAssembly

      • Kedar S. Namjoshi, Anton Xue

      Pages 127-148

4. Concurrent and Distributed Systems

   1. Front Matter

      Pages 149-149

      PDF

   2. Concurrent Correctness in Vector Space

      • Christina Peterson, Victor Cook, Damian Dechev

      Pages 151-173

   3. Verification of Concurrent Programs Using Petri Net Unfoldings

      • Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schätzle

      Pages 174-195

   4. Eliminating Message Counters in Synchronous Threshold Automata

      • Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger

      Pages 196-218

   5. A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries

      • Nathalie Bertrand, Marijana Lazić, Josef Widder

      Pages 219-239

5. Abstract Interpretation and Model Checking

   1. Front Matter

      Pages 241-241

      PDF

   2. Runtime Abstract Interpretation for Numerical Accuracy and Robustness

      • Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles

      Pages 243-266

   3. Twinning Automata and Regular Expressions for String Static Analysis

      • Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi

      Pages 267-290

   4. Unbounded Procedure Summaries from Bounded Environments

      • Lauren Pick, Grigory Fedyukovich, Aarti Gupta

      Pages 291-324

   5. Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking

      • Hongce Zhang, Aarti Gupta, Sharad Malik

      Pages 325-349

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. 

• architecture verification and validation
• automata theory
• distributed computer systems
• embedded systems
• formal languages
• formal logic
• formal methods
• model checking
• software architecture
• software defect analysis
• software design
• software engineering
• software quality
• software verification
• verification and validation

• University of Copenhagen, Copenhagen, Denmark

  Fritz Henglein

• Tel Aviv University, Tel Aviv, Israel

  Sharon Shoham

• Technion, Haifa, Israel

  Yakir Vizel

Policies and ethics