default search action
CAV 2024, Montreal, QC, Canada - Part I
- Arie Gurfinkel
, Vijay Ganesh
Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14681, Springer 2024, ISBN 978-3-031-65626-2
Decision Procedures
- Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig:
Split Gröbner Bases for Satisfiability Modulo Finite Fields. 3-25 - Nikolaj S. Bjørner, Lev Nachmanson:
Arithmetic Solving in Z3. 26-41 - Peter Habermehl
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. 42-67 - Mengyu Zhao, Shaowei Cai, Yuhang Qian:
Distributed SMT Solving Based on Dynamic Variable-Level Partitioning. 68-88 - Charlie Murphy, Zachary Kincaid
Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement. 89-109 - Joseph E. Reeves
From Clauses to Klauses [inline-graphic not available: see fulltext]. 110-132 - Armin Biere
CaDiCaL 2.0. 133-152 - Yong Kiam Tan
Formally Certified Approximate Model Counting. 153-177 - Aina Niemetz
Scalable Bit-Blasting with Abstractions. 178-200
Hardware Model Checking
- Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier:
The MoXI Model Exchange Tool Suite. 203-218 - Franz Brauße
SMLP: Symbolic Machine Learning Prover. 219-233 - Yechuan Xia, Alessandro Cimatti, Alberto Griggio, Jianwen Li:
Avoiding the Shoals - A New Approach to Liveness Checking. 234-254 - Kenneth L. McMillan:
Toward Liveness Proofs at Scale. 255-276
Software Verification
- Arjun Pitchanathan
Strided Difference Bound Matrices. 279-302 - Yannick Stade
The Top-Down Solver Verified: Building Confidence in Static Analyzers. 303-324 - Shenghao Yuan
End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT. 325-347 - Chanhee Cho, Yi Zhou, Jay Bosamiya, Bryan Parno:
A Framework for Debugging Automated Program Verification Proofs via Proof Actions. 348-361 - Marco Eilers
Verification Algorithms for Automated Separation Logic Verifiers. 362-386 - Michele Chiari
SMT-Based Symbolic Model-Checking for Operator Precedence Languages. 387-408 - Chenglin Wang
On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches. 409-430 - Shaowei Zhu
Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates. 431-452 - Dxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall, Mikael Brockman:
Hevm, a Fast Symbolic Execution Framework for EVM Bytecode. 453-465 - Konstantin Britikov
SolTG: A CHC-Based Solidity Test Case Generator. 466-479 - Sujit Kumar Muduli
Interactive Theorem Proving Modulo Fuzzing. 480-493
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: