VMCAI 2020

21 papers

1. A Cooperative Parallelization Approach for Property-Directed k-Induction · Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina
2. A Systematic Approach to Abstract Interpretation of Program Transformations · Sven Keidel, Sebastian Erdweg
3. BackFlow: Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results · Pietro Ferrara, Luca Olivieri, Fausto Spoto
4. Cheap CTL Compassion in NuSMV · Daniel Hausmann, Tadeusz Litak, Christoph Rauch, Matthias Zinner
5. Fixing Code that Explodes Under Symbolic Evaluation · Sorawee Porncharoenwase, James Bornholt, Emina Torlak
6. Formalizing and Checking Multilevel Consistency · Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Ranjal Gautham Shenoy, S. P. Suresh
7. Generalized Property-Directed Reachability for Hybrid Systems · Kohei Suenaga, Takuya Ishizawa
8. Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation · Oren Ish-Shalom, Shachar Itzhaky, Roman Manevich, Noam Rinetzky
9. How to Win First-Order Safety Games · Helmut Seidl, Christian Müller, Bernd Finkbeiner
10. Improving Parity Game Solvers with Justifications · Ruben Lapauw, Maurice Bruynooghe, Marc Denecker
11. Language Inclusion for Finite Prime Event Structures · Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher
12. Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification · Jack J. Garzella, Marek S. Baranowski, Shaobo He, Zvonimir Rakamaric
13. Practical Abstractions for Automated Verification of Shared-Memory Concurrency · Wytse Oortwijn, Dilian Gurov, Marieke Huisman
14. Promptness and Bounded Fairness in Concurrent and Parameterized Systems · Swen Jacobs, Mouhammad Sakr, Martin Zimmermann
15. Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction · Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
16. Sharing Ghost Variables in a Collection of Abstract Domains · Marc Chevalier, Jérôme Feret
17. Solving $\mathrm {LIA} ^\star $ Using Approximations · Maxwell Levatich, Nikolaj S. Bjørner, Ruzica Piskac, Sharon Shoham
18. Synthesizing Environment Invariants for Modular Hardware Verification · Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik
19. Systematic Classification of Attackers via Bounded Model Checking · Eric Rothstein Morris, Jun Sun, Sudipta Chattopadhyay
20. The Correctness of a Code Generator for a Functional Language · Nathanaël Courant, Antoine Séré, Natarajan Shankar
21. Witnessing Secure Compilation · Kedar S. Namjoshi, Lucas M. Tabajara