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
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
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). 110-134
AI Verification
- David Shriver
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
Automated Safety Verification of Programs Invoking Neural Networks. 201-224 - Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh
Scalable Polyhedral Verification of Recurrent Neural Networks. 225-248 - Radoslav Ivanov, Taylor J. Carpenter
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
PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier. 287-300
Concurrency and Blockchain
- Alasdair Armstrong, Brian Campbell
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. 303-316 - Neta Elad
Summing up Smart Transitions. 317-340 - Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis
Stateless Model Checking Under a Reads-Value-From Equivalence. 341-366 - Felix A. Wolf
Gobra: Modular Specification and Verification of Go Programs. 367-379 - Andrew Johnson, Thomas Wahl:
Delay-Bounded Scheduling Without Delay! 380-402 - Tiago Cogumbreiro
Checking Data-Race Freedom of GPU Kernels, Compositionally. 403-426 - Michalis Kokologiannakis
GenMC: A Model Checker for Weak Memory Models. 427-440
Hybrid and Cyber-Physical Systems
- Qiuye Wang
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. 443-466 - Zhengfeng Yang, Yidan Zhang, Wang Lin, Xia Zeng
An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation. 467-490 - Jaehun Lee, Sharon Kim, Kyungmin Bae
HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL. 491-504 - Nikola Benes
Computing Bottom SCCs Symbolically Using Transition Guided Reduction. 505-528 - Sergio Mover, Alessandro Cimatti, Alberto Griggio
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. 529-551 - Étienne André
IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability. 552-565 - Ratan Lal
Formally Verified Switching Logic for Recoverability of Aircraft Controller. 566-579 - Hussein Sibai
SceneChecker: Boosting Scenario Verification Using Symmetry Abstractions. 580-594 - Zhenya Zhang
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness. 595-618 - S. Akshay
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
A Temporal Logic for Asynchronous Hyperproperties. 694-717 - Marco Eilers
Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. 718-741 - Hiroshi Unno, Tachio Terauchi
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
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
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
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.
last updated on 2024-12-19 22:02 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: