Venues / CAV /

CAV 2021

84 papers

A Temporal Logic for Asynchronous Hyperproperties · Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez
AIGEN: Random Generation of Symbolic Transition Systems · Swen Jacobs, Mouhammad Sakr
ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures · Lorenz Leutgeb, Georg Moser, Florian Zuleger
Adapting Behaviors via Reactive Synthesis · Gal Amram, Suguman Bansal, Dror Fried, Lucas Martinelli Tabajara, Moshe Y. Vardi, Gera Weiss
Algebraic Program Analysis · Zachary Kincaid, Thomas W. Reps, John Cyphert
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 + 1 more
An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation · Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes
An SMT Solver for Regular Expressions and Linear Arithmetic over String Length · Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka + 1 more
Automated Safety Verification of Programs Invoking Neural Networks · Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li + 2 more
Automatic Generation and Validation of Instruction Encoders and Decoders · Xiangzhe Xu, Jinhua Wu, Yuting Wang, Zhenguo Yin, Pengfei Li
Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios · Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wüstholz
BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks · Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song, Taolue Chen
Balancing Automation and Control for Formal Verification of Microprocessors · Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords
Cameleer: A Deductive Verification Tool for OCaml · Mário Pereira, António Ravara
Causality-Based Game Solving · Christel Baier, Norine Coenen, Bernd Finkbeiner, Florian Funke, Simon Jantsch, Julian Siber
Checking Data-Race Freedom of GPU Kernels, Compositionally · Tiago Cogumbreiro, Julien Lange, Dennis Liew Zhen Rong, Hannah Zicarelli
Computing Bottom SCCs Symbolically Using Transition Guided Reduction · Nikola Benes, Lubos Brim, Samuel Pastva, David Safránek
Constraint-Based Relational Verification · Hiroshi Unno, Tachio Terauchi, Eric Koskinen
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver · Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
Counterexample-Guided Partial Bounding for Recursive Function Synthesis · Azadeh Farzan, Victor Nicolet
Counting Minimal Unsatisfiable Subsets · Jaroslav Bendík, Kuldeep S. Meel
DNNV: A Framework for Deep Neural Network Verification · David Shriver, Sebastian G. Elbaum, Matthew B. Dwyer
Debugging Network Reachability with Blocked Paths · Sam Bayless, John D. Backes, Dan DaCosta, Benjamin F. Jones, Nate Launchbury, Patrick Trentin + 4 more
Decision Tree Learning in CEGIS-Based Termination Analysis · Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper) · Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
Delay-Bounded Scheduling Without Delay! · Andrew Johnson, Thomas Wahl
Diffy: Inductive Reasoning of Array Programs Using Difference Invariants · Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness · Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, Jianjun Zhao
Efficient SMT-Based Analysis of Failure Propagation · Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonás, Greg Kimberly
Enforcing Almost-Sure Reachability in POMDPs · Sebastian Junges, Nils Jansen, Sanjit A. Seshia
Fast Computation of Strong Control Dependencies · Marek Chalupa, David Klaska, Jan Strejcek, Lukás Tomovic
Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata · S. Akshay, Paul Gastin, Karthik R. Prakash
Formally Validating a Practical Verification Condition Generator · Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
Formally Verified Switching Logic for Recoverability of Aircraft Controller · Ratan Lal, Aaron McKinnis, Dustin Hauptman, Shawn Keshmiri, Pavithra Prabhakar
Foundations of Fine-Grained Explainability · Sylvain Hallé, Hugo Tremblay
Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms · Anshuman Mohan, Wei Xiang Leow, Aquinas Hobor
GPU Acceleration of Bounded Model Checking with ParaFROST · Muhammad Osama, Anton Wijs
GenMC: A Model Checker for Weak Memory Models · Michalis Kokologiannakis, Viktor Vafeiadis
Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting · Tobias Reinhard, Bart Jacobs
Gillian, Part II: Real-World Verification for JavaScript and C · Petar Maksimovic, Sacha-Élie Ayoun, José Fragoso Santos, Philippa Gardner
Gobra: Modular Specification and Verification of Go Programs · Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João Carlos Pereira, Peter Müller
HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL · Jaehun Lee, Sharon Kim, Kyungmin Bae, Peter Csaba Ölveczky
IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability · Étienne André
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems · Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Stefano Tonetta
Interpolation and Model Checking for Nonlinear Arithmetic · Dejan Jovanovic, Bruno Dutertre
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models · Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
JavaSMT 3: Interacting with SMT Solvers in Java · Daniel Baier, Dirk Beyer, Karlheinz Friedberger
LLMC: Verifying High-Performance Software · Freark I. van der Berg
Latticed k-Induction with an Application to Probabilistic Programs · Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
Learning Probabilistic Termination Proofs · Alessandro Abate, Mirco Giacobbe, Diptarko Roy
Learning Union of Integer Hypercubes with Queries - (with Applications to Monadic Decomposition) · Oliver Markgraf, Daniel Stan, Anthony W. Lin
Lower-Bound Synthesis Using Loop Specialization and Max-SMT · Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo, Albert Rubio
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference · Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd D. Millstein, Sanjit A. Seshia, Guy Van den Broeck
Model Checking ømega-Regular Properties with Decoupled Search · Daniel Gnad, Jan Eisenhut, Alberto Lluch-Lafuente, Jörg Hoffmann
Model-Checking Structured Context-Free Languages · Michele Chiari, Dino Mandrioli, Matteo Pradella
Model-Free Reinforcement Learning for Branching Markov Decision Processes · Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
NNrepair: Constraint-Based Repair of Neural Network Classifiers · Muhammad Usman, Divya Gopinath, Youcheng Sun, Yannic Noller, Corina S. Pasareanu
Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference · Guillaume Girol, Benjamin Farinier, Sébastien Bardin
PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs · Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen, Simon Stupinský
PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier · Haitham Khedr, James Ferlez, Yasser Shoukry
Pono: A Flexible and Extensible SMT-Based Model Checker · Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown + 2 more
Porous Invariants · Engel Lefaucheux, Joël Ouaknine, David Purser, James Worrell
Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning · Claudia Cauli, Meng Li, Nir Piterman, Oksana Tkachuk
Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security · Marco Eilers, Severin Meier, Peter Müller
Program Sketching by Automatically Generating Mocks from Tests · Nate F. F. Bragg, Jeffrey S. Foster, Cody Roux, Armando Solar-Lezama
Programmable Program Synthesis · Loris D'Antoni, Qinheping Hu, Jinwoo Kim, Thomas W. Reps
Progress in Certifying Hardware Model Checking Results · Emily Yu, Armin Biere, Keijo Heljanko
Reflections on Termination of Linear Loops · Shaowei Zhu, Zachary Kincaid
Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations · George A. Constantinides, Fredrik Dahlqvist, Zvonimir Rakamaric, Rocco Salvia
Robustness Verification of Quantum Classifiers · Ji Guan, Wang Fang, Mingsheng Ying
Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability · Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Diego Manzanas Lopez, Nathaniel Hamilton, Xiaodong Yang + 2 more
Runtime Monitors for Markov Decision Processes · Sebastian Junges, Hazem Torfah, Sanjit A. Seshia
Scalable Polyhedral Verification of Recurrent Neural Networks · Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei Marian Dan, Martin T. Vechev
SceneChecker: Boosting Scenario Verification Using Symmetry Abstractions · Hussein Sibai, Yangge Li, Sayan Mitra
Sound Verification Procedures for Temporal Properties of Infinite-State Systems · Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, David Chemouil
Stateless Model Checking Under a Reads-Value-From Equivalence · Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, Viktor Toman
Summing up Smart Transitions · Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv
Synthesis with Asymptotic Resource Bounds · Qinheping Hu, John Cyphert, Loris D'Antoni, Thomas W. Reps
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming · Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
Theory Exploration Powered by Deductive Synthesis · Eytan Singher, Shachar Itzhaky
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation · Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu
Verified Cryptographic Code for Everybody · Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher + 1 more
Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning · Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas, Insup Lee
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends · Gereon Kremer, Aina Niemetz, Mathias Preiner