PUBLICATIONS from Code Verification for Practical Machine Architectures
See the main project page for information
about the UT Austin CRASH project.
Authors from our CRASH group at UT Austin are shown in bold
font.
- Well-Formedness Guarantees for ACL2 Metafunctions and Clause
Processors.
Matt Kaufmann and J Strother Moore.
DIFTS'15: International
Workshop on Design and Implementation of Formal Tools and Systems.
- Fourier Series Formalization in ACL2(r)
Cuong K. Chau, Matt Kaufmann, and Warren A. Hunt,
Jr.
Proceedings of ACL2 Workshop 2015.
- Efficient,
Mechanically-Verified Validation of Satisfiability Solvers.
Nathan David Wetzler.
PhD dissertation, The University of Texas at Austin, May 2015.
- Expressing symmetry breaking in DRAT proofs
Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan
Wetzler
International Conference on Automated Deduction (CADE), volume 9195 of
LNCS, 2015.
- Simulation and Formal Verification of x86 Machine-Code
Programs that make System Calls.
Shilpi Goel, Warren A. Hunt, Jr., Matt Kaufmann,
and Soumava Ghosh.
Proceedings of FMCAD 2014, Formal Methods in Computer-Aided Design,
2014.
- Efficient Extraction of Skolem Functions from QRAT
Proofs.
Marijn J. H. Heule, Martina Seidl, and Armin Biere.
Proceedings of FMCAD 2014, Formal Methods in Computer-Aided Design,
2014.
- Validating Unsatisfiability Results of Clause Sharing
Parallel SAT Solvers.
Marijn J. H. Heule, Norbert Manthey, and Tobias Philipp.
Proceedings of PoS 2014, 5th Pragmatics of SAT workshop, 2014.
- Rough Diamond: An Extension of Equivalence-based Rewriting.
Matt Kaufmann and J Strother Moore.
Proceedings of ITP 2014, 5th Conference on Interactive Theorem
Proving, 2014.
- DRAT-trim: Efficient Checking and Trimming Using
Expressive Clausal Proofs.
Nathan Wetzler, Marijn J. H. Heule, and Warren
A. Hunt, Jr..
International Conference on Theory and Applications of Satisfiability
Testing (SAT), 2014.
- Everything You Always Wanted to Know About Blocked Sets
(But Were Afraid to Ask).
Tomas Balyo, Andreas Frohlich, Marijn J. H. Heule, and Armin Biere.
International Conference on Theory and Applications of Satisfiability
Testing (SAT), 2014.
- MUS Extraction using Clausal Proofs.
Anton Belov, Marijn J. H. Heule, and Joao Marques-Silva.
International Conference on Theory and Applications of Satisfiability
Testing (SAT), 2014.
- A Unified Proof System for QBF Preprocessing
Marijn J. H. Heule, Martina Seidl, and Armin Biere.
7th International Joint Conference on Automated Reasoning (IJCAR
2014).
- Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4.
Matt Kaufmann and J Strother Moore.
ACL2 Workshop 2014.
- Industrial-Strength Documentation for ACL2.
Jared Davis and Matt Kaufmann.
ACL2 Workshop 2014.
- Blocked Clause Decomposition.
Marijn J. H. Heule and Armin Biere.
LPAR-19, Logic for Programming Artificial Intelligence and Reasoning, 2014.
- Trimming while Checking Clausal Proofs.
Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan Wetzler.
FMCAD 2013, 13th Conference on Formal Methods in Computer-Aided Design.
- Bridging the Gap Between Easy Generation and Efficient Verification of Unsatisfiability Proofs.
Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler.
Software Testing, Verification, and Reliability (STVR): Special Issue
on Tests and Proofs, 2014.
- Guided Merging of Sequence Diagrams.
Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, and Hans Tompits.
Conference on Software Language Engineering 2012.
- Concurrent Cube-and-Conquer.
Peter van der Tak, Marijn J.H. Heule, and Armin Biere.
Pragmatics of SAT 2012.
- A Formal Model of a Large Memory that Supports Efficient Execution.
Warren A. Hunt, Jr. and Matt Kaufmann.
Formal Methods in Computer-Aided Design 2012.
- Towards a Formal Model of the X86 ISA.
Warren A. Hunt, Jr. and Matt Kaufmann.
Technical Report, Dept. of Computer Science, University of Texas at Austin.
- Automated Reencoding of Boolean Formulas.
Norbert Manthey, Marijn J. H. Heule and Armin Biere.
Haifa Verification Conference 2012.
- Revisiting Hyper Binary Resolution.
Marijn J. H. Heule, Matti Jarvisalo, and Armin Biere.
Conference on Integration of Artificial Intelligence and Operations Research techniques in Constraint Programming (2013).
- Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1.
Matt Kaufmann and J Strother Moore.
ACL2 Workshop 2013, Electronic Proceedings in Theoretical Computer Science.
- A Parallelized Theorem Prover for a Logic with Parallel Execution.
David L. Rager (now at Oracle), Warren A. Hunt, Jr., and Matt Kaufmann.
ITP 2013, 4th Conference on Interactive Theorem Proving.
- Abstract Stobjs and Their Application to ISA Modeling.
Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann.
ACL2 Workshop 2013, Electronic Proceedings in Theoretical Computer Science.
- Automated Code Proofs on a Formal Model of the X86
Shilpi Goel and Warren A. Hunt, Jr.
VSTTE 2013 (Verified Software: Theories, Tools, and Experiments).
- Verifying Refutations with Extended Resolution.
Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan Wetzler.
Conference on Automated Deduction 2013.
- Mechanical Verification of SAT Refutations with Extended Resolution.
Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr.
ITP 2013, 4th Conference on Interactive Theorem Proving.
- A SAT Approach to Clique-Width.
Marijn J. H. Heule and Stefan Szeider.
International Conference on Theory and Applications of Satisfiability Testing (2013).