Abstract is missing.
- Semi-Open-State Testing for in-Silicon Coherent InterconnectsJasmin Schult, Ben Fiedler, David A. Cock, Timothy Roscoe. 1-10 [doi]
- Writing Proofs in DafnyK. Rustan M. Leino. 1 [doi]
- Extending DRAT to SMTS. Hitarth, Cayden R. Codel, Hanna Lachnitt, Bruno Dutertre. 1-11 [doi]
- Some Adventures in Learning Proving, Instantiation and SynthesisJosef Urban. 1 [doi]
- Towards Verification Modulo Theories of Asynchronous Systems via Abstraction RefinementGianluca Redondi, Alessandro Cimatti, Alberto Griggio. 1-5 [doi]
- Clausal Equivalence SweepingArmin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks. 1-6 [doi]
- Formally Verified Rounding Errors of the Logarithm-Sum-Exponential FunctionPaul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, Raphaël Rieu-Helft. 1-10 [doi]
- Hardware Model Checking Competition 2024Armin Biere, Nils Froleyks, Mathias Preiner. 1 [doi]
- Tackling Scalability Issues in Bit-Vector ReasoningAina Niemetz. 1 [doi]
- Memory Consistency Model-Aware Cache Coherence for Heterogeneous HardwareRachel Cleaveland, Caroline Trippel. 1-12 [doi]
- Harnessing SMT Solvers for Reasoning about DeFi ProtocolsMooly Sagiv. 1 [doi]
- SMT-D: New Strategies for Portfolio-Based SMT SolvingClark W. Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert B. Jones, Nham Le, Andrew Reynolds 0001, Kunal Sheth, Christopher Stephens, Michael W. Whalen. 1-10 [doi]
- Context Pruning for More Robust SMT-based Program VerificationYi Zhou 0025, Jay Bosamiya, Jessica Li, Marijn J. H. Heule, Bryan Parno. 1-11 [doi]
- Translating Natural Language to Temporal Logics with Large Language Models and Model CheckersDaniel Mendoza, Christopher Hahn, Caroline Trippel. 1-11 [doi]
- The FMCAD 2024 Student ForumMartin Blicha, Nestan Tsiskaridze. 5-6 [doi]
- Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction SelectionRoss Daly, Caleb Donovick, Caleb Terrill, Jackson Melchert, Priyanka Raina, Clark W. Barrett, Pat Hanrahan. 8-17 [doi]
- Solving String Constraints with Concatenation Using SATKevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Dirk Nowotka. 29-38 [doi]
- Modernizing SMT-Based Type Error LocalizationMax Kopinsky, Brigitte Pientka, Xujie Si. 49-58 [doi]
- Easter Egg: Equality Reasoning Based on E-Graphs with Multiple AssumptionsEytan Singher, Shachar Itzhaky. 70-83 [doi]
- Word Equations as Abstract Domain for String Manipulating ProgramsAntonina Nepeivoda. 84-94 [doi]
- Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier CertificatesUdayan Mandal, Guy Amir, Haoze Wu 0001, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett. 95-106 [doi]
- Leveraging LLMs for Program VerificationAdharsh Kamath, Nausheen Mohammed, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy 0001, Rahul Sharma 0001. 107-118 [doi]
- Recomposition: A New Technique for Efficient Compositional VerificationIan Dardik, April Porter, Eunsuk Kang. 130-141 [doi]
- Evaluating LLM-driven User-Intent Formalization for Verification-Aware LanguagesShuvendu K. Lahiri. 142-147 [doi]
- Translating Pseudo-Boolean Proofs into Boolean Clausal ProofsKarthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule. 175-185 [doi]
- Verified Substitution Redundancy CheckingCayden R. Codel, Jeremy Avigad, Marijn J. H. Heule. 186-196 [doi]
- 2-DQBF Solving and Certification via Property-Directed Reachability AnalysisLong-Hin Fung, Che Cheng, Yu-Wei Fan, Tony Tan, Jie-Hong Roland Jiang. 197-207 [doi]
- Projective Model Counting for IP Addresses in Access Control PoliciesLoris D'Antoni, Andrew Gacek, Amit Goel, Dejan Jovanovic, Rami Gökhan Kici, Daniel Peebles, Neha Rungta, Yasmine Sharoda, Chungha Sung. 208-216 [doi]
- Toward Exhaustive Sequential Redundancy RemovalRohit Dureja, Jason Baumgartner, Raj Kumar Gajavelly, Robert Kanzelman, Kristin Y. Rozier. 217-226 [doi]
- DAG-Based Compositional Approaches for LTLf to DFA ConversionsSuguman Bansal, Yash Kankariya, Yong Li 0031. 227-235 [doi]
- Automatic Verification of Right-Greedy Numerical Linear Algebra AlgorithmsCarl Kwan, Warren A. Hunt Jr.. 242-250 [doi]
- Symbolic Computer Algebra for Multipliers Revisited - It's All About Orders and PhasesAlexander Konrad, Christoph Scholl 0001. 261-271 [doi]
- Combining Symbolic Execution with Predicate Abstraction and CEGARMartin Jonás, Jan Strejcek, Alberto Griggio. 271-280 [doi]
- Efficient Synthesis of Symbolic Distributed Protocols by SketchingDerek Egolf, William Schultz, Stavros Tripakis. 281-291 [doi]
- Ownership in Low-Level Intermediate RepresentationSiddharth Priya, Arie Gurfinkel. 292-300 [doi]