Abstract is missing.
- Split Gröbner Bases for Satisfiability Modulo Finite FieldsAlex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark W. Barrett, Isil Dillig. 3-25 [doi]
- Arithmetic Solving in Z3Nikolaj S. Bjørner, Lev Nachmanson. 26-41 [doi]
- Algebraic Reasoning Meets Automata in Solving Linear Integer ArithmeticPeter Habermehl, Vojtech Havlena, Michal Hecko, Lukás Holík, Ondrej Lengál. 42-67 [doi]
- Distributed SMT Solving Based on Dynamic Variable-Level PartitioningMengyu Zhao, Shaowei Cai 0001, Yuhang Qian. 68-88 [doi]
- Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy ImprovementCharlie Murphy, Zachary Kincaid. 89-109 [doi]
- From Clauses to Klauses [inline-graphic not available: see fulltext]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant. 110-132 [doi]
- CaDiCaL 2.0Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt. 133-152 [doi]
- Formally Certified Approximate Model CountingYong Kiam Tan, Jiong Yang 0002, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel. 153-177 [doi]
- Scalable Bit-Blasting with AbstractionsAina Niemetz, Mathias Preiner, Yoni Zohar. 178-200 [doi]
- The MoXI Model Exchange Tool SuiteChris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier. 203-218 [doi]
- SMLP: Symbolic Machine Learning ProverFranz Brauße, Zurab Khasidashvili, Konstantin Korovin. 219-233 [doi]
- Avoiding the Shoals - A New Approach to Liveness CheckingYechuan Xia, Alessandro Cimatti, Alberto Griggio, Jianwen Li. 234-254 [doi]
- Toward Liveness Proofs at ScaleKenneth L. McMillan. 255-276 [doi]
- Strided Difference Bound MatricesArjun Pitchanathan, Albert Cohen 0001, Oleksandr Zinenko, Tobias Grosser. 279-302 [doi]
- The Top-Down Solver Verified: Building Confidence in Static AnalyzersYannick Stade, Sarah Tilscher, Helmut Seidl. 303-324 [doi]
- End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoTShenghao Yuan, Frédéric Besson, Jean-Pierre Talpin. 325-347 [doi]
- A Framework for Debugging Automated Program Verification Proofs via Proof ActionsChanhee Cho, Yi Zhou 0025, Jay Bosamiya, Bryan Parno. 348-361 [doi]
- Verification Algorithms for Automated Separation Logic VerifiersMarco Eilers, Malte Schwerhoff, Peter Müller 0001. 362-386 [doi]
- SMT-Based Symbolic Model-Checking for Operator Precedence LanguagesMichele Chiari, Luca Geatti, Nicola Gigante, Matteo Pradella. 387-408 [doi]
- On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic BranchesChenglin Wang, Fangzhen Lin. 409-430 [doi]
- Breaking the Mold: Nonlinear Ranking Function Synthesis Without TemplatesShaowei Zhu 0001, Zachary Kincaid. 431-452 [doi]
- Hevm, a Fast Symbolic Execution Framework for EVM BytecodeDxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall, Mikael Brockman. 453-465 [doi]
- SolTG: A CHC-Based Solidity Test Case GeneratorKonstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt, Natasha Sharygina. 466-479 [doi]
- Interactive Theorem Proving Modulo FuzzingSujit Kumar Muduli, Rohan Ravikumar Padulkar, Subhajit Roy 0001. 480-493 [doi]