Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID33rd 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
a service of 
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-08-17 23:46 CEST 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:
