These following papers have been accepted to CAV 2021.
- Towards a Trustworthy Semantics-Based Language Framework via Proof Generation (Artifact). Xiaohong Chen, Zhengyao Lin, Thai Trinh and Grigore Rosu
- Cameleer: a Deductive Verification Tool for OCaml (Artifact). Mário Pereira and António Ravara
- Progress in Certifying Hardware Model Checking Results. Emily Yu, Armin Biere and Keijo Heljanko
- Isla: Integrating full-scale ISA semantics and axiomatic concurrency models. Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte and Peter Sewell
- Verified Cryptographic Code for Everybody (Artifact). Brett Boston, Samuel Breese, Josiah Dodds, Mike Dodds, Brian Huffman, Adam Petcher and Andrei Stefanescu
- Theory Exploration Powered by Deductive Synthesis (Artifact). Eytan Singher and Shachar Itzhaky
- Synthesis with Asymptotic Resource Bounds (Artifact). Qinheping Hu, John Cyphert, Loris D’Antoni and Thomas Reps
- CoqQFBV: A Scalable Certified SMT QFBV Solver. Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang and Bo-Yin Yang
- Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference (Artifact). Guillaume Girol, Benjamin Farinier and Sebastien Bardin
- Summing Up Smart Transitions. Neta Elad, Sophie Rain, Neil Immerman, Laura Kovacs and Mooly Sagiv
- LLMC: Verifying High-Performance Software (Artifact). Freark van der Berg
- DNNV: A Framework for Deep Neural Network Verification (Artifact). David Shriver, Sebastian Elbaum and Matthew Dwyer
- Model-Checking Structured Context-Free Languages (Artifact). Michele Chiari, Dino Mandrioli and Matteo Pradella
- Porous Invariants. Engel Lefaucheux, Joël Ouaknine, David Purser and James Worrell
- Program Sketching by Automatically Generating Mocks from Tests (Artifact). Nate Bragg, Jeff Foster, Cody Roux and Armando Solar-Lezama
- Runtime Monitors for Markov Decision Processes (Artifact). Sebastian Junges, Hazem Torfah and Sanjit A. Seshia
- Robustness Verification of Quantum Classifiers. Ji Guan, Wang Fang and Mingsheng Ying
- 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
- BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks. Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song and Taolue Chen
- Formally Validating a Practical Verification Condition Generator (Artifact). Gaurav Parthasarathy, Peter Müller and Alexander Summers
- Automatic Generation and Validation of Instruction Encoders and Decoders (Artifact). Xiangzhe Xu, Jinhua Wu, Yuting Wang, Zhenguo Yin and Pengfei Li
- JavaSMT 3: Interacting with SMT Solvers in Java (Artifact). Karlheinz Friedberger, Dirk Beyer and Daniel Baier
- Learning Probabilistic Termination Proofs (Artifact). Alessandro Abate, Mirco Giacobbe and Diptarko Roy
- An SMT Encoding of LLVM’s Memory Model for Bounded Translation Validation. Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur and Nuno P. Lopes
- Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios (Artifact). Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A Navas and Valentin Wüstholz
- Model Checking Omega-Regular Properties with Decoupled Search. Daniel Gnad, Jan Eisenhut, Alberto Lluch Lafuente and Jörg Hoffmann
- 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
- Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming (Artifact). Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen
- 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
- AIGEN: Random Generation of Symbolic Transition Systems (Artifact). Mouhammad Sakr and Swen Jacobs
- HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL (Artifact). Jaehun Lee, Sharon Kim, Kyungmin Bae and Peter Ölveczky
- Counterexample-Guided Partial Bounding for Recursive Function Synthesis (Artifact). Victor Nicolet and Azadeh Farzan
- Functional Correctness of C implementations of Dijkstra’s, Kruskal’s, and Prim’s Algorithms (Artifact). Anshuman Mohan, Wei Xiang Leow and Aquinas Hobor
- Ghost Signals: Verifying Termination of Busy Waiting. Tobias Reinhard and Bart Jacobs
- A Temporal Logic for Asynchronous Hyperproperties. Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner and Cesar Sanchez
- Computing Bottom SCCs Symbolically Using Transition Guided Reduction (Artifact). Nikola Benes, Lubos Brim, Samuel Pastva and David Šafránek
- Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan and Stefano Tonetta
- 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
- IMITATOR 3: Synthesis of timing parameters beyond decidability (Artifact). Étienne André
- PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs (Artifact). Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen and Simon Stupinsky
- Efficient SMT-based Analysis of Failure Propagation. Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonáš and Greg Kimberly
- Stateless Model Checking under a Reads-Value-From Equivalence. Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis and Viktor Toman
- Adapting Behaviors via Reactive Synthesis (Artifact). Gal Amram, Suguman Bansal, Dror Fried, Lucas Martinelli Tabajara, Moshe Vardi and Gera Weiss
- GPU Acceleration of Bounded Model Checking with GPU4BMC. Muhammad Osama and Anton Wijs
- 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
- Scalable Polyhedral Verification of Recurrent Neural Networks (Artifact). Wonryong Ryou, Jiayu Chen, Mislav Balunović, Gagandeep Singh, Andrei Dan and Martin Vechev
- Gillian Verification for JavaScript and C (Artifact). Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos and Philippa Gardner
- Delay-Bounded Scheduling Without Delay! (Artifact). Andrew Johnson and Thomas Wahl
- 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
- ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends (Artifact). Gereon Kremer, Aina Niemetz and Mathias Preiner
- Checking Data-Race Freedom of GPU Kernels, Compositionally (Artifact). Tiago Cogumbreiro, Julien Lange, Dennis Liew Zhen Rong and Hannah Zicarelli
- Enforcing Almost-Sure Reachability in POMDPs (Artifact). Sebastian Junges, Nils Jansen and Sanjit A. Seshia
- Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security (Artifact). Marco Eilers, Severin Meier and Peter Müller
- Formally Verified Switching Logic for Recoverability of Aircraft Controller. Ratan Lal, Aaron McKinnis, Dustin Hauptman, Shawn Keshmiri and Pavithra Prabhakar
- Interpolation and Model Checking for Nonlinear Arithmetic. Dejan Jovanović and Bruno Dutertre
- 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
- 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
- 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
- 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
- Constraint-based Relational Verification (Artifact). Hiroshi Unno, Tachio Terauchi and Eric Koskinen
- Reflections on Termination of Linear Loops (Artifact). Shaowei Zhu and Zachary Kincaid
- Decision Tree Learning in CEGIS-Based Termination Analysis (Artifact). Satoshi Kura, Hiroshi Unno and Ichiro Hasuo
- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier (Artifact). Haitham Khedr, James Ferlez and Yasser Shoukry
- Lower-Bound Synthesis using Loop Specialization and Max-SMT. Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo and Albert Rubio
- SceneChecker: Boosting Scenario Verification using Symmetry Abstractions (Artifact). Hussein Sibai, Yangge Li and Sayan Mitra
- Causality-based Game Solving (Artifact). Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch and Julian Siber
- Fast Computation of Strong Control Dependencies (Artifact). Marek Chalupa, David Klaška, Jan Strejček and Lukáš Tomovič
- Model-free Reinforcement Learning for Branching Markov Decision Processes (Artifact). Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak
- ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures (Artifact). Lorenz Leutgeb, Georg Moser and Florian Zuleger
- Counting Minimal Unsatisfiable Subsets. Jaroslav Bendík and Kuldeep S. Meel
- 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
- Sound Verification Procedures of Temporal Properties of FOLTL Specifications (Artifact). Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel and David Chemouil
- Diffy: Inductive Reasoning of Array Programs using Difference Invariants (Artifact). Supratik Chakraborty, Ashutosh Gupta and Divyesh Unadkat
- GenMC: A Model Checker for Weak Memory Models (Artifact). Michalis Kokologiannakis and Viktor Vafeiadis
- Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning. Claudia Cauli, Meng Li, Nir Piterman and Oksana Tkachuk
- Fast zone-based algorithms for reachability in pushdown timed automata (Artifact). S. Akshay, Paul Gastin and Karthik Prakash
- Formal Foundations of Fine-Grained Explainability (Artifact). Sylvain Hallé and Hugo Tremblay
- Rigorous Floating-Point Roundoff Error Analysis of Probabilistic Computations (Artifact). Rocco Salvia, Fredrik Dahlqvist, Zvonimir Rakamaric and George Constantinides
- Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition) (Artifact). Oliver Markgraf, Anthony Widjaja Lin and Daniel Stan