David A. Greve

Publication Activity (10 Years)

Years Active: 1998-2022
Publications (10 Years): 6

Top Topics

Technical Systems

Linear Constraints

Semantic Indexing

Microsoft Sql Server

Top Venues

Publications

David A. Greve, Jennifer A. Davis, Laura R. Humphrey
A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A. ACL2 (2022)
Andrew T. Walter, David A. Greve, Panagiotis Manolios
Enumerative Data Types with Constraints. FMCAD (2022)
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
Synthesis of Infinite-State Systems with Random Behavior. ASE (2020)
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen
Synthesis of Infinite-State Systems with Random Behavior. CoRR (2020)
David A. Greve, Andrew Gacek
Trapezoidal Generalization over Linear Constraints. ACL2 (2018)
Lucas G. Wagner, David A. Greve, Andrew Gacek
SIMPAL: a compositional reasoning framework for imperative programs. SPIN (2017)
David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg
Development of a Translator from LLVM to ACL2. ACL2 (2014)
David A. Greve, Konrad Slind
A Step-Indexing Approach to Partial Functions ACL2 (2013)
David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding
Efficient execution in an automated reasoning environment. J. Funct. Program. 18 (1) (2008)
Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David A. Greve
Specification and Checking of Software Contracts for Conditional Information Flow. FM (2008)
David A. Greve
Parameterized congruences in ACL2. ACL2 (2006)
Matthew Wilding, David A. Greve, David S. Hardin
Efficient Simulation of Formal Processor Models. Formal Methods Syst. Des. 18 (3) (2001)
David A. Greve
Symbolic Simulation of the JEM1 Microprocessor. FMCAD (1998)
David S. Hardin, Matthew Wilding, David A. Greve
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. CAV (1998)