David A. Greve

According to our database, David A. Greve authored at least 17 papers between 1998 and 2022.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

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

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

Enumerative Data Types with Constraints.

Andrew T. Walter, David A. Greve, Panagiotis Manolios

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

2020

Synthesis of Infinite-State Systems with Random Behavior.

Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen

Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

2018

Trapezoidal Generalization over Linear Constraints.

David A. Greve, Andrew Gacek

Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, 2018

2017

SIMPAL: a compositional reasoning framework for imperative programs.

Lucas G. Wagner, David A. Greve, Andrew Gacek

Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

2014

Development of a Translator from LLVM to ACL2.

David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

2013

A Step-Indexing Approach to Partial Functions

David A. Greve, Konrad Slind

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

2010

Formal Verification of Partition Management for the AAMP7G Microprocessor.

Matthew Wilding, David A. Greve, Raymond J. Richards, David S. Hardin

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

Model Checking Information Flow.

Michael W. Whalen, David A. Greve, Lucas G. Wagner

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

Information Security Modeling and Analysis.

David A. Greve

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

Specification and Checking of Software Contracts for Conditional Information Flow.

Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David A. Greve

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

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, 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

Proceedings of the FM 2008: Formal Methods, 2008

2006

Parameterized congruences in ACL2.

David A. Greve

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

2001

Efficient Simulation of Formal Processor Models.

Matthew Wilding, David A. Greve, David S. Hardin

Formal Methods Syst. Des., 2001

1998

Symbolic Simulation of the JEM1 Microprocessor.

David A. Greve

Proceedings of the Formal Methods in Computer-Aided Design, 1998

Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle.

David S. Hardin, Matthew Wilding, David A. Greve

Proceedings of the Computer Aided Verification, 10th International Conference, 1998