


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
, Vojtech Havlena
, Michal Hecko
, Lukás Holík
, Ondrej Lengál
:
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
, Marijn J. H. Heule
, Randal E. Bryant
:
From Clauses to Klauses [inline-graphic not available: see fulltext]. 110-132 - Armin Biere
, Tobias Faller
, Katalin Fazekas
, Mathias Fleury
, Nils Froleyks
, Florian Pollitt
:
CaDiCaL 2.0. 133-152 - Yong Kiam Tan
, Jiong Yang
, Mate Soos
, Magnus O. Myreen
, Kuldeep S. Meel
:
Formally Certified Approximate Model Counting. 153-177 - Aina Niemetz
, Mathias Preiner
, Yoni Zohar
:
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
, Zurab Khasidashvili
, Konstantin Korovin
:
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
, Albert Cohen
, Oleksandr Zinenko
, Tobias Grosser
:
Strided Difference Bound Matrices. 279-302 - Yannick Stade
, Sarah Tilscher
, Helmut Seidl
:
The Top-Down Solver Verified: Building Confidence in Static Analyzers. 303-324 - Shenghao Yuan
, Frédéric Besson
, Jean-Pierre Talpin
:
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
, Malte Schwerhoff
, Peter Müller
:
Verification Algorithms for Automated Separation Logic Verifiers. 362-386 - Michele Chiari
, Luca Geatti
, Nicola Gigante
, Matteo Pradella
:
SMT-Based Symbolic Model-Checking for Operator Precedence Languages. 387-408 - Chenglin Wang
, Fangzhen Lin
:
On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches. 409-430 - Shaowei Zhu
, Zachary Kincaid
:
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
, Ilia Zlatkin
, Grigory Fedyukovich
, Leonardo Alt
, Natasha Sharygina
:
SolTG: A CHC-Based Solidity Test Case Generator. 466-479 - Sujit Kumar Muduli
, Rohan Ravikumar Padulkar
, Subhajit Roy
:
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.