David A. Greve

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