


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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.