Accepted Papers

These following papers have been accepted to CAV 2021.

  1. Towards a Trustworthy Semantics-Based Language Framework via Proof Generation (Artifact). Xiaohong Chen, Zhengyao Lin, Thai Trinh and Grigore Rosu
  2. Cameleer: a Deductive Verification Tool for OCaml (Artifact). Mário Pereira and António Ravara
  3. Progress in Certifying Hardware Model Checking Results. Emily Yu, Armin Biere and Keijo Heljanko
  4. Isla: Integrating full-scale ISA semantics and axiomatic concurrency models. Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte and Peter Sewell
  5. Verified Cryptographic Code for Everybody (Artifact). Brett Boston, Samuel Breese, Josiah Dodds, Mike Dodds, Brian Huffman, Adam Petcher and Andrei Stefanescu
  6. Theory Exploration Powered by Deductive Synthesis (Artifact). Eytan Singher and Shachar Itzhaky
  7. Synthesis with Asymptotic Resource Bounds (Artifact). Qinheping Hu, John Cyphert, Loris D’Antoni and Thomas Reps
  8. CoqQFBV: A Scalable Certified SMT QFBV Solver. Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang and Bo-Yin Yang
  9. Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference (Artifact). Guillaume Girol, Benjamin Farinier and Sebastien Bardin
  10. Summing Up Smart Transitions. Neta Elad, Sophie Rain, Neil Immerman, Laura Kovacs and Mooly Sagiv
  11. LLMC: Verifying High-Performance Software (Artifact). Freark van der Berg
  12. DNNV: A Framework for Deep Neural Network Verification (Artifact). David Shriver, Sebastian Elbaum and Matthew Dwyer
  13. Model-Checking Structured Context-Free Languages (Artifact). Michele Chiari, Dino Mandrioli and Matteo Pradella
  14. Porous Invariants. Engel Lefaucheux, Joël Ouaknine, David Purser and James Worrell
  15. Program Sketching by Automatically Generating Mocks from Tests (Artifact). Nate Bragg, Jeff Foster, Cody Roux and Armando Solar-Lezama
  16. Runtime Monitors for Markov Decision Processes (Artifact). Sebastian Junges, Hazem Torfah and Sanjit A. Seshia
  17. Robustness Verification of Quantum Classifiers. Ji Guan, Wang Fang and Mingsheng Ying
  18. Model Checking Finite-Horizon Markov Chains with Probabilistic Inference (Artifact). Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd Millstein, Sanjit A. Seshia and Guy Van den Broeck
  19. BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks. Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song and Taolue Chen
  20. Formally Validating a Practical Verification Condition Generator (Artifact). Gaurav Parthasarathy, Peter Müller and Alexander Summers
  21. Automatic Generation and Validation of Instruction Encoders and Decoders (Artifact). Xiangzhe Xu, Jinhua Wu, Yuting Wang, Zhenguo Yin and Pengfei Li
  22. JavaSMT 3: Interacting with SMT Solvers in Java (Artifact). Karlheinz Friedberger, Dirk Beyer and Daniel Baier
  23. Learning Probabilistic Termination Proofs (Artifact). Alessandro Abate, Mirco Giacobbe and Diptarko Roy
  24. An SMT Encoding of LLVM’s Memory Model for Bounded Translation Validation. Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur and Nuno P. Lopes
  25. Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios (Artifact). Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A Navas and Valentin Wüstholz
  26. Model Checking Omega-Regular Properties with Decoupled Search. Daniel Gnad, Jan Eisenhut, Alberto Lluch Lafuente and Jörg Hoffmann
  27. Automated Safety Verification of Programs Invoking Neural Networks. Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li, Jorge A Navas and Valentin Wüstholz
  28. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming (Artifact). Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen
  29. An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation. Zhengfeng Yang, Yidan Zhang, Wang Lin, Xia Zeng, Xiaochao Tang, Zhenbing Zeng and Zhiming Liu
  30. AIGEN: Random Generation of Symbolic Transition Systems (Artifact). Mouhammad Sakr and Swen Jacobs
  31. HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL (Artifact). Jaehun Lee, Sharon Kim, Kyungmin Bae and Peter Ölveczky
  32. Counterexample-Guided Partial Bounding for Recursive Function Synthesis (Artifact). Victor Nicolet and Azadeh Farzan
  33. Functional Correctness of C implementations of Dijkstra’s, Kruskal’s, and Prim’s Algorithms (Artifact). Anshuman Mohan, Wei Xiang Leow and Aquinas Hobor
  34. Ghost Signals: Verifying Termination of Busy Waiting. Tobias Reinhard and Bart Jacobs
  35. A Temporal Logic for Asynchronous Hyperproperties. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner and Cesar Sanchez
  36. Computing Bottom SCCs Symbolically Using Transition Guided Reduction (Artifact). Nikola Benes, Lubos Brim, Samuel Pastva and David Šafránek
  37. Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan and Stefano Tonetta
  38. Latticed k-Induction with an Application to Probabilistic Programs (Artifact). Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer
  39. IMITATOR 3: Synthesis of timing parameters beyond decidability (Artifact). Étienne André
  40. PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs (Artifact). Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen and Simon Stupinsky
  41. Efficient SMT-based Analysis of Failure Propagation. Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonáš and Greg Kimberly
  42. Stateless Model Checking under a Reads-Value-From Equivalence. Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis and Viktor Toman
  43. Adapting Behaviors via Reactive Synthesis (Artifact). Gal Amram, Suguman Bansal, Dror Fried, Lucas Martinelli Tabajara, Moshe Vardi and Gera Weiss
  44. GPU Acceleration of Bounded Model Checking with GPU4BMC. Muhammad Osama and Anton Wijs
  45. Gobra: Modular Specification and Verification of Go Programs (Artifact). Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira and Peter Müller
  46. Scalable Polyhedral Verification of Recurrent Neural Networks (Artifact). Wonryong Ryou, Jiayu Chen, Mislav Balunović, Gagandeep Singh, Andrei Dan and Martin Vechev
  47. Gillian Verification for JavaScript and C (Artifact). Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos and Philippa Gardner
  48. Delay-Bounded Scheduling Without Delay! (Artifact). Andrew Johnson and Thomas Wahl
  49. Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning. Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas and Insup Lee
  50. ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends (Artifact). Gereon Kremer, Aina Niemetz and Mathias Preiner
  51. Checking Data-Race Freedom of GPU Kernels, Compositionally (Artifact). Tiago Cogumbreiro, Julien Lange, Dennis Liew Zhen Rong and Hannah Zicarelli
  52. Enforcing Almost-Sure Reachability in POMDPs (Artifact). Sebastian Junges, Nils Jansen and Sanjit A. Seshia
  53. Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security (Artifact). Marco Eilers, Severin Meier and Peter Müller
  54. Formally Verified Switching Logic for Recoverability of Aircraft Controller. Ratan Lal, Aaron McKinnis, Dustin Hauptman, Shawn Keshmiri and Pavithra Prabhakar
  55. Interpolation and Model Checking for Nonlinear Arithmetic. Dejan Jovanović and Bruno Dutertre
  56. Pono: A Flexible and Extensible SMT-based Model Checker (Artifact). Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta and Clark Barrett
  57. Debugging Network Reachability with Blocked Paths. Sam Bayless, John Backes, Dan DaCosta, Benjamin F Jones, Nate Launchbury, Patrick Trentin, Kelsey Jewell, Sagar Joshi, Michael Q. Zeng and Nandita Mathews
  58. An SMT Solver for Regular Expressions and Linear Arithmetic over String Length (Artifact). Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka and Vijay Ganesh
  59. Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability (Artifact). Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Xiaodong Yang, Nathaniel P Hamilton, Diego Manzanas Lopez, Stanley Bak and Taylor T Johnson
  60. Constraint-based Relational Verification (Artifact). Hiroshi Unno, Tachio Terauchi and Eric Koskinen
  61. Reflections on Termination of Linear Loops (Artifact). Shaowei Zhu and Zachary Kincaid
  62. Decision Tree Learning in CEGIS-Based Termination Analysis (Artifact). Satoshi Kura, Hiroshi Unno and Ichiro Hasuo
  63. PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier (Artifact). Haitham Khedr, James Ferlez and Yasser Shoukry
  64. Lower-Bound Synthesis using Loop Specialization and Max-SMT. Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo and Albert Rubio
  65. SceneChecker: Boosting Scenario Verification using Symmetry Abstractions (Artifact). Hussein Sibai, Yangge Li and Sayan Mitra
  66. Causality-based Game Solving (Artifact). Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch and Julian Siber
  67. Fast Computation of Strong Control Dependencies (Artifact). Marek Chalupa, David Klaška, Jan Strejček and Lukáš Tomovič
  68. Model-free Reinforcement Learning for Branching Markov Decision Processes (Artifact). Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak
  69. ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures (Artifact). Lorenz Leutgeb, Georg Moser and Florian Zuleger
  70. Counting Minimal Unsatisfiable Subsets. Jaroslav Bendík and Kuldeep S. Meel
  71. Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness. Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo and Jianjun Zhao
  72. Sound Verification Procedures of Temporal Properties of FOLTL Specifications (Artifact). Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel and David Chemouil
  73. Diffy: Inductive Reasoning of Array Programs using Difference Invariants (Artifact). Supratik Chakraborty, Ashutosh Gupta and Divyesh Unadkat
  74. GenMC: A Model Checker for Weak Memory Models (Artifact). Michalis Kokologiannakis and Viktor Vafeiadis
  75. Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning. Claudia Cauli, Meng Li, Nir Piterman and Oksana Tkachuk
  76. Fast zone-based algorithms for reachability in pushdown timed automata (Artifact). S. Akshay, Paul Gastin and Karthik Prakash
  77. Formal Foundations of Fine-Grained Explainability (Artifact). Sylvain Hallé and Hugo Tremblay
  78. Rigorous Floating-Point Roundoff Error Analysis of Probabilistic Computations (Artifact). Rocco Salvia, Fredrik Dahlqvist, Zvonimir Rakamaric and George Constantinides
  79. Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition) (Artifact). Oliver Markgraf, Anthony Widjaja Lin and Daniel Stan