| Long-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan and Jie-Hong Roland Jiang |
2-DQBF Solving and Certification via Property-Directed Reachability Analysis |
|
| Carl Kwan and Warren Hunt |
Automatic Verification of Right-greedy Numerical Linear Algebra Algorithms |
|
| Shuvendu Lahiri |
Benchmarking LLM-driven User-Intent Formalization for Verification-Aware Languages (short paper) |
|
| Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Froleyks |
Clausal Equivalence Sweeping (short paper) |
|
| Martin Jonáš, Jan Strejček and Alberto Griggio |
Combining Symbolic Execution with Predicate Abstraction and CEGAR |
|
| Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule and Bryan Parno |
Context Pruning for More Robust SMT-based Program Verification |
|
| Clark Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Mike Whalen and Chriss Stephens |
SMT-D: New Strategies for Portfolio-Based SMT Solving (tool paper) |
|
| Yash Kankariya, Yong Li and Suguman Bansal |
DAG-Based Compositional Approaches for LTLf to DFA Conversions (tool paper) |
|
| Eytan Singher and Shachar Itzhaky |
Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions |
|
| Derek Egolf, William Schultz and Stavros Tripakis |
Efficient Synthesis of Symbolic Distributed Protocols by Sketching |
|
| Ross Daly, Caleb Donovick, Caleb Terrill, Jack Melchert, Priyanka Raina, Clark Barrett and Pat Hanrahan |
Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection |
|
| Jasmin Schult, Ben Fiedler, David Cock and Timothy Roscoe |
Extended open-state testing for in-silicon coherent interconnects |
|
| S Hitarth, Cayden Codel, Hanna Lachnitt and Bruno Dutertre |
Extending DRAT to SMT |
|
| Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché and Raphaël Rieu-Helft |
Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function |
|
| Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Newell, Umberto Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz and Clark Barrett |
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates |
|
| Adharsh Kamath, Nausheen Mohammed, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy and Rahul Sharma |
Leveraging LLMs for Program Verification |
|
| Rachel Cleaveland and Caroline Trippel |
Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware |
|
| Max Kopinsky, Brigitte Pientka and Xujie Si |
Modernizing SMT-Based Type Error Localization (tool paper) |
|
| Siddharth Priya and Arie Gurfinkel |
Ownership in low-level intermediate representation |
|
| Loris D’Antoni, Andrew Gacek, Amit Goel, Dejan Jovanovic, Dan Peebles, Neha Rungta and Yasmine Sharoda |
Projective Model Counting for IP Addresses in Access Control Policies |
|
| Ian Dardik, April Porter and Eunsuk Kang |
Recomposition: A New Technique for Efficient Compositional Verification |
|
| Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong and Dirk Nowotka |
Solving String Constraints with Concatenation Using SAT |
|
| Alexander Konrad and Christoph Scholl |
Symbolic Computer Algebra for Multipliers Revisited - It’s All About Orders and Phases |
|
| Rohit Dureja, Jason Baumgartner, Raj Kumar Gajavelly, Robert Kanzelman and Kristin Yvonne Rozier |
Toward Exhaustive Sequential Redundancy Removal |
|
| Gianluca Redondi, Alessandro Cimatti and Alberto Griggio |
Towards Verification Modulo Theories of asynchronous systems via abstraction refinement (short paper) |
|
| Daniel Mendoza, Christopher Hahn and Caroline Trippel |
Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers |
|
| Karthik Nukala, Soumyaditya Choudhuri, Randal Bryant and Marijn Heule |
Translating Pseudo-Boolean Proofs to Clausal Proofs |
|
| Cayden Codel, Jeremy Avigad and Marijn Heule |
Verified substitution redundancy checking |
|
| Antonina Nepeivoda |
Word Equations as Abstract Domain for String Manipulating Programs |
|
