default search action
33rd CAV 2021: Virtual Event - Part II
- Alexandra Silva, K. Rustan M. Leino:
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science 12760, Springer 2021, ISBN 978-3-030-81687-2
Complexity and Termination
- Alessandro Abate, Mirco Giacobbe
, Diptarko Roy:
Learning Probabilistic Termination Proofs. 3-26 - Tobias Reinhard
Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting. 27-50 - Shaowei Zhu
Reflections on Termination of Linear Loops. 51-74 - Satoshi Kura
Decision Tree Learning in CEGIS-Based Termination Analysis. 75-98 - Lorenz Leutgeb
ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. 99-122
Decision Procedures and Solvers
- Eytan Singher
Theory Exploration Powered by Deductive Synthesis. 125-148 - Xiaomu Shi, Yu-Fu Fu
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. 149-171 - Engel Lefaucheux
Porous Invariants. 172-194 - Daniel Baier
JavaSMT 3: Interacting with SMT Solvers in Java. 195-208 - Marco Bozzano
Efficient SMT-Based Analysis of Failure Propagation. 209-230 - Gereon Kremer
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. 231-242 - Oliver Markgraf
Learning Union of Integer Hypercubes with Queries - (with Applications to Monadic Decomposition). 243-265 - Dejan Jovanovic, Bruno Dutertre:
Interpolation and Model Checking for Nonlinear Arithmetic. 266-288 - Murphy Berzish, Mitja Kulczynski
An SMT Solver for Regular Expressions and Linear Arithmetic over String Length. 289-312 - Jaroslav Bendík, Kuldeep S. Meel:
Counting Minimal Unsatisfiable Subsets. 313-336 - Quentin Peyras, Jean-Paul Bodeveix, Julien Brunel, David Chemouil
Sound Verification Procedures for Temporal Properties of Infinite-State Systems. 337-360
Hardware and Model Checking
- Emily Yu, Armin Biere, Keijo Heljanko
Progress in Certifying Hardware Model Checking Results. 363-386 - Michele Chiari
Model-Checking Structured Context-Free Languages. 387-410 - Daniel Gnad
Model Checking ømega-Regular Properties with Decoupled Search. 411-434 - Swen Jacobs, Mouhammad Sakr:
AIGEN: Random Generation of Symbolic Transition Systems. 435-446 - Muhammad Osama
GPU Acceleration of Bounded Model Checking with ParaFROST. 447-460 - Makai Mann
Pono: A Flexible and Extensible SMT-Based Model Checker. 461-474
Logical Foundations
- Xiaohong Chen
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. 477-499 - Sylvain Hallé, Hugo Tremblay
Foundations of Fine-Grained Explainability. 500-523 - Kevin Batz
Latticed k-Induction with an Application to Probabilistic Programs. 524-549
Stochastic Systems
- Sebastian Junges
Runtime Monitors for Markov Decision Processes. 553-576 - Steven Holtzen
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. 577-601 - Sebastian Junges
Enforcing Almost-Sure Reachability in POMDPs. 602-625 - George A. Constantinides, Fredrik Dahlqvist, Zvonimir Rakamaric, Rocco Salvia:
Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations. 626-650 - Ernst Moritz Hahn
Model-Free Reinforcement Learning for Branching Markov Decision Processes. 651-673
Software Verification
- Mário Pereira
Cameleer: A Deductive Verification Tool for OCaml. 677-689 - Freark I. van der Berg:
LLMC: Verifying High-Performance Software. 690-703 - Gaurav Parthasarathy, Peter Müller, Alexander J. Summers:
Formally Validating a Practical Verification Condition Generator. 704-727 - Xiangzhe Xu
Automatic Generation and Validation of Instruction Encoders and Decoders. 728-751 - Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes:
An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation. 752-776 - Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wüstholz:
Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios. 777-800 - Anshuman Mohan, Wei Xiang Leow, Aquinas Hobor:
Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms. 801-826 - Petar Maksimovic, Sacha-Élie Ayoun, José Fragoso Santos, Philippa Gardner:
Gillian, Part II: Real-World Verification for JavaScript and C. 827-850 - Sam Bayless, John D. Backes, Dan DaCosta, Benjamin F. Jones, Nate Launchbury, Patrick Trentin, Kelsey Jewell, Sagar Joshi, Michael Q. Zeng, Nandita Mathews:
Debugging Network Reachability with Blocked Paths. 851-862 - Elvira Albert
Lower-Bound Synthesis Using Loop Specialization and Max-SMT. 863-886 - Marek Chalupa
Fast Computation of Strong Control Dependencies. 887-910 - Supratik Chakraborty
Diffy: Inductive Reasoning of Array Programs Using Difference Invariants. 911-935
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-11-22 19:31 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: