![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
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
, Bart Jacobs
:
Ghost Signals: Verifying Termination of Busy Waiting - Verifying Termination of Busy Waiting. 27-50 - Shaowei Zhu
, Zachary Kincaid
:
Reflections on Termination of Linear Loops. 51-74 - Satoshi Kura
, Hiroshi Unno, Ichiro Hasuo:
Decision Tree Learning in CEGIS-Based Termination Analysis. 75-98 - Lorenz Leutgeb
, Georg Moser
, Florian Zuleger:
ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures. 99-122
Decision Procedures and Solvers
- Eytan Singher, Shachar Itzhaky:
Theory Exploration Powered by Deductive Synthesis. 125-148 - Xiaomu Shi, Yu-Fu Fu
, Jiaxiang Liu
, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang:
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. 149-171 - Engel Lefaucheux
, Joël Ouaknine
, David Purser
, James Worrell
:
Porous Invariants. 172-194 - Daniel Baier
, Dirk Beyer
, Karlheinz Friedberger
:
JavaSMT 3: Interacting with SMT Solvers in Java. 195-208 - Marco Bozzano
, Alessandro Cimatti
, Anthony Fernandes Pires, Alberto Griggio
, Martin Jonás
, Greg Kimberly:
Efficient SMT-Based Analysis of Failure Propagation. 209-230 - Gereon Kremer
, Aina Niemetz
, Mathias Preiner
:
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. 231-242 - Oliver Markgraf
, Daniel Stan
, Anthony W. Lin
:
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
, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, Vijay Ganesh
:
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
, Dino Mandrioli
, Matteo Pradella
:
Model-Checking Structured Context-Free Languages. 387-410 - Daniel Gnad
, Jan Eisenhut, Alberto Lluch-Lafuente
, Jörg Hoffmann:
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
, Anton Wijs
:
GPU Acceleration of Bounded Model Checking with ParaFROST. 447-460 - Makai Mann
, Ahmed Irfan
, Florian Lonsing
, Yahan Yang, Hongce Zhang
, Kristopher Brown
, Aarti Gupta
, Clark W. Barrett
:
Pono: A Flexible and Extensible SMT-Based Model Checker. 461-474
Logical Foundations
- Xiaohong Chen
, Zhengyao Lin
, Minh-Thai Trinh
, Grigore Rosu
:
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
, Mingshuai Chen
, Benjamin Lucien Kaminski
, Joost-Pieter Katoen
, Christoph Matheja
, Philipp Schröer
:
Latticed k-Induction with an Application to Probabilistic Programs. 524-549
Stochastic Systems
- Sebastian Junges
, Hazem Torfah
, Sanjit A. Seshia
:
Runtime Monitors for Markov Decision Processes. 553-576 - Steven Holtzen
, Sebastian Junges
, Marcell Vazquez-Chanlatte
, Todd D. Millstein
, Sanjit A. Seshia
, Guy Van den Broeck
:
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference. 577-601 - Sebastian Junges
, Nils Jansen
, Sanjit A. Seshia
:
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
, Mateo Perez
, Sven Schewe
, Fabio Somenzi
, Ashutosh Trivedi
, Dominik Wojtczak
:
Model-Free Reinforcement Learning for Branching Markov Decision Processes. 651-673
Software Verification
- Mário Pereira
, António Ravara
:
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
, Jinhua Wu
, Yuting Wang
, Zhenguo Yin, Pengfei Li:
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
, Samir Genaim
, Enrique Martin-Martin
, Alicia Merayo, Albert Rubio
:
Lower-Bound Synthesis Using Loop Specialization and Max-SMT. 863-886 - Marek Chalupa
, David Klaska, Jan Strejcek
, Lukás Tomovic:
Fast Computation of Strong Control Dependencies. 887-910 - Supratik Chakraborty
, Ashutosh Gupta, Divyesh Unadkat
:
Diffy: Inductive Reasoning of Array Programs Using Difference Invariants. 911-935
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
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.