Stop the war!

Остановите войну!

for scientists:

default search action

combined dblp search
author search
venue search
publication search

ask others

David A. Greve

> Home > Persons

Person information

affiliation: Rockwell Collins, Cedar Rapids, IA, USA

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

Journal Articles

see FAQ

What is the meaning of the colors in the publication lists?

2008
[j2]
- view
  authority control:
- export record
  dblp key:
  - journals/jfp/GreveKMMRRSVW08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfp/GreveKMMRRSVW08
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): 15-46 (2008)
2001
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/WildingGH01
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/WildingGH01
Matthew Wilding, David A. Greve, David S. Hardin:
Efficient Simulation of Formal Processor Models. Formal Methods Syst. Des. 18(3): 233-248 (2001)

Conference and Workshop Papers

see FAQ

What is the meaning of the colors in the publication lists?

2022
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/WalterGM22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/WalterGM22
Andrew T. Walter, David A. Greve, Panagiotis Manolios:
Enumerative Data Types with Constraints. FMCAD 2022: 189-198
[c10]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2205-11697
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2205-11697
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: 33-47
2020
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/kbse/KatisFCGRW20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/kbse/KatisFCGRW20
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen:
Synthesis of Infinite-State Systems with Random Behavior. ASE 2020: 250-261
2018
[c8]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1810-04310
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1810-04310
David A. Greve, Andrew Gacek:
Trapezoidal Generalization over Linear Constraints. ACL2 2018: 30-46
2017
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/spin/WagnerGG17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/spin/WagnerGG17
Lucas G. Wagner, David A. Greve, Andrew Gacek:
SIMPAL: a compositional reasoning framework for imperative programs. SPIN 2017: 90-93
2014
[c6]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/HardinDGM14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/HardinDGM14
David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg:
Development of a Translator from LLVM to ACL2. ACL2 2014: 163-177
2013
[c5]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1304-7857
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1304-7857
David A. Greve, Konrad Slind:
A Step-Indexing Approach to Partial Functions. ACL2 2013: 42-53
2008
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/AmtoftHRRHG08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/AmtoftHRRHG08
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: 229-245
2006
[c3]
- view
  authority control:
- export record
  dblp key:
  - conf/acl2/Greve06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/acl2/Greve06
David A. Greve:
Parameterized congruences in ACL2. ACL2 2006: 28-34
1998
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/HardinWG98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/HardinWG98
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: 39-44
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/Greve98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/Greve98
David A. Greve:
Symbolic Simulation of the JEM1 Microprocessor. FMCAD 1998: 321-333

Parts in Books or Collections

see FAQ

What is the meaning of the colors in the publication lists?

2010
[p4]
- view
  authority control:
- export record
  dblp key:
  - books/sp/10/WildingGRH10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/sp/10/WildingGRH10
Matthew Wilding, David A. Greve, Raymond J. Richards, David S. Hardin:
Formal Verification of Partition Management for the AAMP7G Microprocessor. Design and Verification of Microprocessor Systems for High-Assurance Applications 2010: 175-191
[p3]
- view
  authority control:
- export record
  dblp key:
  - books/sp/10/Greve10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/sp/10/Greve10
David A. Greve:
Information Security Modeling and Analysis. Design and Verification of Microprocessor Systems for High-Assurance Applications 2010: 249-299
[p2]
- view
  authority control:
- export record
  dblp key:
  - books/sp/10/AmtoftHRRHG10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/sp/10/AmtoftHRRHG10
Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David A. Greve:
Specification and Checking of Software Contracts for Conditional Information Flow. Design and Verification of Microprocessor Systems for High-Assurance Applications 2010: 341-379
[p1]
- view
  authority control:
- export record
  dblp key:
  - books/sp/10/WhalenGW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/sp/10/WhalenGW10
Michael W. Whalen, David A. Greve, Lucas G. Wagner:
Model Checking Information Flow. Design and Verification of Microprocessor Systems for High-Assurance Applications 2010: 381-428

Informal and Other Publications

see FAQ

What is the meaning of the colors in the publication lists?

2020
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/abs-2009-12330
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2009-12330
Andreas Katis, Grigory Fedyukovich, Jeffrey Chen, David A. Greve, Sanjai Rayadurgam, Michael W. Whalen:
Synthesis of Infinite-State Systems with Random Behavior. CoRR abs/2009.12330 (2020)

Coauthor Index

see FAQ

a service of

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.