| 2021 | A Design of GPU-Based Quantitative Model Checking. YoungMin Kwon, Eunhee Kim |
| 2021 | A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. Nathalie Bertrand, Marijana Lazic, Josef Widder |
| 2021 | A Self-certifying Compilation Framework for WebAssembly. Kedar S. Namjoshi, Anton Xue |
| 2021 | A Synchronous Effects Logic for Temporal Verification of Pure Esterel. Yahui Song, Wei-Ngan Chin |
| 2021 | Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). Andreas Humenberger, Laura Kovács |
| 2021 | Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible. Marius Kamp, Michael Philippsen |
| 2021 | Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis. Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin |
| 2021 | Compositional Model Checking for Multi-properties. Ohad Goudsmid, Orna Grumberg, Sarai Sheinvald |
| 2021 | Compositional Satisfiability Solving in Separation Logic. Quang Loc Le |
| 2021 | Concurrent Correctness in Vector Space. Christina L. Peterson, Victor Cook, Damian Dechev |
| 2021 | Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. Martin Bromberger, Alberto Fiori, Christoph Weidenbach |
| 2021 | Decomposing Data Structure Commutativity Proofs with $m\!n$-Differencing. Eric Koskinen, Kshitij Bansal |
| 2021 | Eliminating Message Counters in Synchronous Threshold Automata. Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
| 2021 | Formal Semantics and Verification of Network-Based Biocomputation Circuits. Michelle Aluf-Medina, Till Korten, Avraham Raviv, Dan V. Nicolau Jr., Hillel Kugler |
| 2021 | GPURepair: Automated Repair of GPU Kernels. Saurabh Joshi, Gautam Muduganti |
| 2021 | Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper). Bernhard Steffen, Alnis Murtovi |
| 2021 | Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching. Jochen Hoenicke, Tanja Schindler |
| 2021 | Model Checking Algorithms for Hyperproperties (Invited Paper). Bernd Finkbeiner |
| 2021 | Netter: Probabilistic, Stateful Network Models. Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, Limin Jia |
| 2021 | On Preprocessing for Weighted MaxSAT. Tobias Paxian, Pascal Raiola, Bernd Becker |
| 2021 | Proving the Existence of Fair Paths in Infinite-State Systems. Alessandro Cimatti, Alberto Griggio, Enrico Magnago |
| 2021 | Runtime Abstract Interpretation for Numerical Accuracy and Robustness. Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles |
| 2021 | Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2021 | Twinning Automata and Regular Expressions for String Static Analysis. Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi |
| 2021 | Unbounded Procedure Summaries from Bounded Environments. Lauren Pick, Grigory Fedyukovich, Aarti Gupta |
| 2021 | Verification of Concurrent Programs Using Petri Net Unfoldings. Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schätzle |
| 2021 | Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings Fritz Henglein, Sharon Shoham, Yakir Vizel |