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.