


default search action
33rd CAV 2021: Virtual Event - Part I
- Alexandra Silva, K. Rustan M. Leino:
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. Lecture Notes in Computer Science 12759, Springer 2021, ISBN 978-3-030-81684-1
Invited Papers
- Muhammad Usman, Divya Gopinath, Youcheng Sun, Yannic Noller, Corina S. Pasareanu:
NNrepair: Constraint-Based Repair of Neural Network Classifiers. 3-25 - Shilpi Goel
, Anna Slobodová, Rob Sumners, Sol Swords
:
Balancing Automation and Control for Formal Verification of Microprocessors. 26-45 - Zachary Kincaid
, Thomas W. Reps, John Cyphert
:
Algebraic Program Analysis. 46-83 - Loris D'Antoni, Qinheping Hu, Jinwoo Kim, Thomas W. Reps:
Programmable Program Synthesis. 84-109 - Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe
, Ilya Sergey:
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). 110-134
AI Verification
- David Shriver
, Sebastian G. Elbaum
, Matthew B. Dwyer
:
DNNV: A Framework for Deep Neural Network Verification. 137-150 - Ji Guan, Wang Fang, Mingsheng Ying
:
Robustness Verification of Quantum Classifiers. 151-174 - Yedi Zhang, Zhe Zhao, Guangke Chen, Fu Song, Taolue Chen
:
BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks. 175-200 - Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li
, Jorge A. Navas, Valentin Wüstholz:
Automated Safety Verification of Programs Invoking Neural Networks. 201-224 - Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh
, Andrei Marian Dan, Martin T. Vechev:
Scalable Polyhedral Verification of Recurrent Neural Networks. 225-248 - Radoslav Ivanov, Taylor J. Carpenter
, James Weimer, Rajeev Alur, George J. Pappas
, Insup Lee:
Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning. 249-262 - Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Diego Manzanas Lopez, Nathaniel Hamilton, Xiaodong Yang, Stanley Bak, Taylor T. Johnson
:
Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability. 263-286 - Haitham Khedr, James Ferlez
, Yasser Shoukry
:
PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier. 287-300
Concurrency and Blockchain
- Alasdair Armstrong, Brian Campbell
, Ben Simner, Christopher Pulte
, Peter Sewell:
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. 303-316 - Neta Elad
, Sophie Rain
, Neil Immerman
, Laura Kovács
, Mooly Sagiv
:
Summing up Smart Transitions. 317-340 - Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis
, Viktor Toman
:
Stateless Model Checking Under a Reads-Value-From Equivalence. 341-366 - Felix A. Wolf
, Linard Arquint
, Martin Clochard, Wytse Oortwijn
, João Carlos Pereira
, Peter Müller
:
Gobra: Modular Specification and Verification of Go Programs. 367-379 - Andrew Johnson, Thomas Wahl:
Delay-Bounded Scheduling Without Delay! 380-402 - Tiago Cogumbreiro
, Julien Lange
, Dennis Liew Zhen Rong
, Hannah Zicarelli
:
Checking Data-Race Freedom of GPU Kernels, Compositionally. 403-426 - Michalis Kokologiannakis
, Viktor Vafeiadis
:
GenMC: A Model Checker for Weak Memory Models. 427-440
Hybrid and Cyber-Physical Systems
- Qiuye Wang
, Mingshuai Chen
, Bai Xue
, Naijun Zhan
, Joost-Pieter Katoen
:
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. 443-466 - Zhengfeng Yang, Yidan Zhang, Wang Lin, Xia Zeng
, Xiaochao Tang, Zhenbing Zeng, Zhiming Liu:
An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation. 467-490 - Jaehun Lee, Sharon Kim, Kyungmin Bae
, Peter Csaba Ölveczky
:
HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL. 491-504 - Nikola Benes
, Lubos Brim, Samuel Pastva, David Safránek
:
Computing Bottom SCCs Symbolically Using Transition Guided Reduction. 505-528 - Sergio Mover, Alessandro Cimatti, Alberto Griggio
, Ahmed Irfan
, Stefano Tonetta:
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. 529-551 - Étienne André
:
IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability. 552-565 - Ratan Lal
, Aaron McKinnis, Dustin Hauptman, Shawn Keshmiri, Pavithra Prabhakar:
Formally Verified Switching Logic for Recoverability of Aircraft Controller. 566-579 - Hussein Sibai
, Yangge Li
, Sayan Mitra
:
SceneChecker: Boosting Scenario Verification Using Symmetry Abstractions. 580-594 - Zhenya Zhang
, Deyun Lyu
, Paolo Arcaini
, Lei Ma
, Ichiro Hasuo
, Jianjun Zhao
:
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness. 595-618 - S. Akshay
, Paul Gastin
, Karthik R. Prakash
:
Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata. 619-642
Security
- Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, Andrei Stefanescu:
Verified Cryptographic Code for Everybody. 645-668 - Guillaume Girol, Benjamin Farinier, Sébastien Bardin:
Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference. 669-693 - Jan Baumeister
, Norine Coenen
, Borzoo Bonakdarpour
, Bernd Finkbeiner
, César Sánchez
:
A Temporal Logic for Asynchronous Hyperproperties. 694-717 - Marco Eilers
, Severin Meier, Peter Müller
:
Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. 718-741 - Hiroshi Unno, Tachio Terauchi
, Eric Koskinen:
Constraint-Based Relational Verification. 742-766 - Claudia Cauli, Meng Li, Nir Piterman, Oksana Tkachuk:
Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning. 767-780
Synthesis
- Qinheping Hu, John Cyphert
, Loris D'Antoni, Thomas W. Reps:
Synthesis with Asymptotic Resource Bounds. 783-807 - Nate F. F. Bragg, Jeffrey S. Foster, Cody Roux, Armando Solar-Lezama:
Program Sketching by Automatically Generating Mocks from Tests. 808-831 - Azadeh Farzan, Victor Nicolet:
Counterexample-Guided Partial Bounding for Recursive Function Synthesis. 832-855 - Roman Andriushchenko
, Milan Ceska
, Sebastian Junges
, Joost-Pieter Katoen
, Simon Stupinský:
PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. 856-869 - Gal Amram, Suguman Bansal, Dror Fried, Lucas Martinelli Tabajara, Moshe Y. Vardi, Gera Weiss:
Adapting Behaviors via Reactive Synthesis. 870-893 - Christel Baier
, Norine Coenen
, Bernd Finkbeiner
, Florian Funke
, Simon Jantsch
, Julian Siber
:
Causality-Based Game Solving. 894-917

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.