Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: David A. Greve
@inproceedings{DBLP:conf/fmcad/WalterGM22,
author = {Andrew T. Walter and
David A. Greve and
Panagiotis Manolios},
editor = {Alberto Griggio and
Neha Rungta},
title = {Enumerative Data Types with Constraints},
booktitle = {22nd Formal Methods in Computer-Aided Design, {FMCAD} 2022, Trento,
Italy, October 17-21, 2022},
pages = {189--198},
publisher = {{IEEE}},
year = {2022},
url = {https://doi.org/10.34727/2022/isbn.978-3-85448-053-2\_25},
doi = {10.34727/2022/ISBN.978-3-85448-053-2\_25},
timestamp = {Fri, 02 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/WalterGM22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2205-11697,
author = {David A. Greve and
Jennifer A. Davis and
Laura R. Humphrey},
editor = {Rob Sumners and
Cuong Chau},
title = {A Mechanized Proof of Bounded Convergence Time for the Distributed
Perimeter Surveillance System {(DPSS)} Algorithm {A}},
booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem
Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022},
series = {{EPTCS}},
volume = {359},
pages = {33--47},
year = {2022},
url = {https://doi.org/10.4204/EPTCS.359.5},
doi = {10.4204/EPTCS.359.5},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-11697.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/kbse/KatisFCGRW20,
author = {Andreas Katis and
Grigory Fedyukovich and
Jeffrey Chen and
David A. Greve and
Sanjai Rayadurgam and
Michael W. Whalen},
title = {Synthesis of Infinite-State Systems with Random Behavior},
booktitle = {35th {IEEE/ACM} International Conference on Automated Software Engineering,
{ASE} 2020, Melbourne, Australia, September 21-25, 2020},
pages = {250--261},
publisher = {{IEEE}},
year = {2020},
url = {https://doi.org/10.1145/3324884.3416586},
doi = {10.1145/3324884.3416586},
timestamp = {Fri, 12 Feb 2021 13:04:43 +0100},
biburl = {https://dblp.org/rec/conf/kbse/KatisFCGRW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2009-12330,
author = {Andreas Katis and
Grigory Fedyukovich and
Jeffrey Chen and
David A. Greve and
Sanjai Rayadurgam and
Michael W. Whalen},
title = {Synthesis of Infinite-State Systems with Random Behavior},
journal = {CoRR},
volume = {abs/2009.12330},
year = {2020},
url = {https://arxiv.org/abs/2009.12330},
eprinttype = {arXiv},
eprint = {2009.12330},
timestamp = {Wed, 30 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2009-12330.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1810-04310,
author = {David A. Greve and
Andrew Gacek},
editor = {Shilpi Goel and
Matt Kaufmann},
title = {Trapezoidal Generalization over Linear Constraints},
booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem
Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018},
series = {{EPTCS}},
volume = {280},
pages = {30--46},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.280.3},
doi = {10.4204/EPTCS.280.3},
timestamp = {Tue, 12 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-04310.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/spin/WagnerGG17,
author = {Lucas G. Wagner and
David A. Greve and
Andrew Gacek},
editor = {Hakan Erdogmus and
Klaus Havelund},
title = {{SIMPAL:} a compositional reasoning framework for imperative programs},
booktitle = {Proceedings of the 24th {ACM} {SIGSOFT} International {SPIN} Symposium
on Model Checking of Software, Santa Barbara, CA, USA, July 10-14,
2017},
pages = {90--93},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3092282.3092290},
doi = {10.1145/3092282.3092290},
timestamp = {Tue, 12 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/spin/WagnerGG17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/HardinDGM14,
author = {David S. Hardin and
Jennifer A. Davis and
David A. Greve and
Jedidiah R. McClurg},
editor = {Freek Verbeek and
Julien Schmaltz},
title = {Development of a Translator from {LLVM} to {ACL2}},
booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover
and its Applications, Vienna, Austria, 12-13th July 2014},
series = {{EPTCS}},
volume = {152},
pages = {163--177},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.152.13},
doi = {10.4204/EPTCS.152.13},
timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
biburl = {https://dblp.org/rec/journals/corr/HardinDGM14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1304-7857,
author = {David A. Greve and
Konrad Slind},
editor = {Ruben Gamboa and
Jared Davis},
title = {A Step-Indexing Approach to Partial Functions},
booktitle = {Proceedings International Workshop on the {ACL2} Theorem Prover and
its Applications, {ACL2} 2013, Laramie, Wyoming, USA, May 30-31, 2013},
series = {{EPTCS}},
volume = {114},
pages = {42--53},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.114.4},
doi = {10.4204/EPTCS.114.4},
timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1304-7857.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/sp/10/WildingGRH10,
author = {Matthew Wilding and
David A. Greve and
Raymond J. Richards and
David S. Hardin},
editor = {David S. Hardin},
title = {Formal Verification of Partition Management for the {AAMP7G} Microprocessor},
booktitle = {Design and Verification of Microprocessor Systems for High-Assurance
Applications},
pages = {175--191},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-1-4419-1539-9\_6},
doi = {10.1007/978-1-4419-1539-9\_6},
timestamp = {Thu, 16 May 2019 21:02:15 +0200},
biburl = {https://dblp.org/rec/books/sp/10/WildingGRH10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/sp/10/Greve10,
author = {David A. Greve},
editor = {David S. Hardin},
title = {Information Security Modeling and Analysis},
booktitle = {Design and Verification of Microprocessor Systems for High-Assurance
Applications},
pages = {249--299},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-1-4419-1539-9\_9},
doi = {10.1007/978-1-4419-1539-9\_9},
timestamp = {Thu, 16 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/sp/10/Greve10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/sp/10/AmtoftHRRHG10,
author = {Torben Amtoft and
John Hatcliff and
Edwin Rodr{\'{\i}}guez and
Robby and
Jonathan Hoag and
David A. Greve},
editor = {David S. Hardin},
title = {Specification and Checking of Software Contracts for Conditional Information
Flow},
booktitle = {Design and Verification of Microprocessor Systems for High-Assurance
Applications},
pages = {341--379},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-1-4419-1539-9\_12},
doi = {10.1007/978-1-4419-1539-9\_12},
timestamp = {Fri, 17 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/sp/10/AmtoftHRRHG10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/sp/10/WhalenGW10,
author = {Michael W. Whalen and
David A. Greve and
Lucas G. Wagner},
editor = {David S. Hardin},
title = {Model Checking Information Flow},
booktitle = {Design and Verification of Microprocessor Systems for High-Assurance
Applications},
pages = {381--428},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-1-4419-1539-9\_13},
doi = {10.1007/978-1-4419-1539-9\_13},
timestamp = {Thu, 16 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/sp/10/WhalenGW10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/GreveKMMRRSVW08,
author = {David A. Greve and
Matt Kaufmann and
Panagiotis Manolios and
J Strother Moore and
Sandip Ray and
Jos{\'{e}}{-}Luis Ruiz{-}Reina and
Rob Sumners and
Daron Vroon and
Matthew Wilding},
title = {Efficient execution in an automated reasoning environment},
journal = {J. Funct. Program.},
volume = {18},
number = {1},
pages = {15--46},
year = {2008},
url = {https://doi.org/10.1017/S0956796807006338},
doi = {10.1017/S0956796807006338},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jfp/GreveKMMRRSVW08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/AmtoftHRRHG08,
author = {Torben Amtoft and
John Hatcliff and
Edwin Rodr{\'{\i}}guez and
Robby and
Jonathan Hoag and
David A. Greve},
editor = {Jorge Cu{\'{e}}llar and
T. S. E. Maibaum and
Kaisa Sere},
title = {Specification and Checking of Software Contracts for Conditional Information
Flow},
booktitle = {{FM} 2008: Formal Methods, 15th International Symposium on Formal
Methods, Turku, Finland, May 26-30, 2008, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5014},
pages = {229--245},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-68237-0\_17},
doi = {10.1007/978-3-540-68237-0\_17},
timestamp = {Tue, 14 May 2019 10:00:46 +0200},
biburl = {https://dblp.org/rec/conf/fm/AmtoftHRRHG08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/acl2/Greve06,
author = {David A. Greve},
editor = {Panagiotis Manolios and
Matthew Wilding},
title = {Parameterized congruences in {ACL2}},
booktitle = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem
Prover and its Applications, {ACL2} 2006, Seattle, Washington, USA,
August 15-16, 2006},
pages = {28--34},
publisher = {{ACM}},
year = {2006},
url = {https://doi.org/10.1145/1217975.1217981},
doi = {10.1145/1217975.1217981},
timestamp = {Tue, 23 Jun 2020 17:42:40 +0200},
biburl = {https://dblp.org/rec/conf/acl2/Greve06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/WildingGH01,
author = {Matthew Wilding and
David A. Greve and
David S. Hardin},
title = {Efficient Simulation of Formal Processor Models},
journal = {Formal Methods Syst. Des.},
volume = {18},
number = {3},
pages = {233--248},
year = {2001},
url = {https://doi.org/10.1023/A:1011217102270},
doi = {10.1023/A:1011217102270},
timestamp = {Fri, 13 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/WildingGH01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/HardinWG98,
author = {David S. Hardin and
Matthew Wilding and
David A. Greve},
editor = {Alan J. Hu and
Moshe Y. Vardi},
title = {Transforming the Theorem Prover into a Digital Design Tool: From Concept
Car to Off-Road Vehicle},
booktitle = {Computer Aided Verification, 10th International Conference, {CAV}
'98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1427},
pages = {39--44},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/BFb0028729},
doi = {10.1007/BFB0028729},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/HardinWG98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/Greve98,
author = {David A. Greve},
editor = {Ganesh Gopalakrishnan and
Phillip J. Windley},
title = {Symbolic Simulation of the {JEM1} Microprocessor},
booktitle = {Formal Methods in Computer-Aided Design, Second International Conference,
{FMCAD} '98, Palo Alto, California, USA, November 4-6, 1998, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1522},
pages = {321--333},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/3-540-49519-3\_21},
doi = {10.1007/3-540-49519-3\_21},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/Greve98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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.
last updated on 2023-09-28 03:08 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
