Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. - David S. Hardin; Matthew Wilding; David A. Greve (CAV, 1998)

Symbolic Simulation of the JEM1 Microprocessor. - David A. Greve (FMCAD, 1998)

Efficient Simulation of Formal Processor Models. - Matthew Wilding; David A. Greve; David S. Hardin (Formal Methods Syst. Des., 2001)

Parameterized congruences in ACL2. - David A. Greve (ACL2, 2006)

Specification and Checking of Software Contracts for Conditional Information Flow. - Torben Amtoft; John Hatcliff; Edwin Rodríguez; Robby; Jonathan Hoag; David A. Greve (FM, 2008)

Efficient execution in an automated reasoning environment. - David A. Greve; Matt Kaufmann; Panagiotis Manolios; J Strother Moore; Sandip Ray; José-Luis Ruiz-Reina; Rob Sumners; Daron Vroon 001; Matthew Wilding (J. Funct. Program., 2008)

Specification and Checking of Software Contracts for Conditional Information Flow. - Torben Amtoft; John Hatcliff; Edwin Rodríguez; Robby; Jonathan Hoag; David A. Greve (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Information Security Modeling and Analysis. - David A. Greve (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Model Checking Information Flow. - Michael W. Whalen; David A. Greve; Lucas G. Wagner (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Formal Verification of Partition Management for the AAMP7G Microprocessor. - Matthew Wilding; David A. Greve; Raymond J. Richards; David S. Hardin (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

A Step-Indexing Approach to Partial Functions - David A. Greve; Konrad Slind (ACL2, 2013)

Development of a Translator from LLVM to ACL2. - David S. Hardin; Jennifer A. Davis; David A. Greve; Jedidiah R. McClurg (ACL2, 2014)

SIMPAL: a compositional reasoning framework for imperative programs. - Lucas G. Wagner; David A. Greve; Andrew Gacek (SPIN, 2017)

Trapezoidal Generalization over Linear Constraints. - David A. Greve; Andrew Gacek (ACL2, 2018)

Synthesis of Infinite-State Systems with Random Behavior. - Andreas Katis; Grigory Fedyukovich; Jeffrey Chen; David A. Greve; Sanjai Rayadurgam; Michael W. Whalen (ASE, 2020)

Enumerative Data Types with Constraints. - Andrew T. Walter; David A. Greve; Panagiotis Manolios (FMCAD, 2022)

A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A. - David A. Greve; Jennifer A. Davis; Laura R. Humphrey (ACL2, 2022)