@misc(esrap, title = {ESRAP -- a packrat parser for Common Lisp}, url = {https://github.com/scymtym/esrap}, note = {Accessed on April 25th, 2022}, ) @misc(hunchentoot, title = {Hunchentoot -- The Common Lisp web server formerly known as TBNL}, url = {http://edicl.github.io/hunchentoot/}, note = {Accessed on April 25th, 2022}, ) @misc(usocket, title = {USOCKET -- Universal socket library for Common Lisp}, url = {https://usocket.common-lisp.dev/}, note = {Accessed on April 25th, 2022}, ) @misc(xtext, title = {Xtext}, url = {https://www.eclipse.org/Xtext/}, note = {Accessed on April 25th, 2022}, ) @inproceedings(chamarthi-integrating-testing, author = {Harsh Raju Chamarthi and Peter C. Dillinger and Matt Kaufmann and Panagiotis Manolios}, year = {2011}, title = {Integrating Testing and Interactive Theorem Proving}, editor = {David S. Hardin and Julien Schmaltz}, booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover and its Applications}, series = {{EPTCS}}, volume = {70}, pages = {4--19}, doi = {10.4204/EPTCS.70.1}, ) @inproceedings(chamarthi-defdata, author = {Harsh Raju Chamarthi and Peter C. Dillinger and Panagiotis Manolios}, year = {2014}, title = {Data Definitions in the {ACL2} Sedan}, editor = {Freek Verbeek and Julien Schmaltz}, booktitle = {Proceedings Twelfth International Workshop on the {ACL2} Theorem Prover and its Applications}, series = {{EPTCS}}, volume = {152}, pages = {27--48}, doi = {10.4204/EPTCS.152.3}, ) @inproceedings(davis-acl2-bridge, author = {Jared Davis}, year = {2013}, title = {Embedding ACL2 models in end-user applications}, booktitle = {Proc. of Do-Form'13}, series = {Do-Form}, publisher = {AISB}, pages = {49--56}, ) @inproceedings(dillinger-hacking, author = {Peter Dillinger and Matt Kaufmann and Pete Manolios}, year = {2007}, title = {Hacking and Extending {ACL2}}, booktitle = {Proceedings of the Seventh International Workshop on the {ACL2} Theorem Prover and its Applications}, ) @article(dillinger-acl2-sedan, author = {Peter C. Dillinger and Panagiotis Manolios and Daron Vroon and J. Strother Moore}, year = {2007}, title = {ACL2s: ``The ACL2 Sedan''}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {2}, pages = {3--18}, doi = {10.1016/j.entcs.2006.09.018}, note = {Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)}, ) @article(gamboa-acl2-nonstandard-analysis, author = {Ruben A Gamboa and Matt Kaufmann}, year = {2001}, title = {Nonstandard analysis in ACL2}, journal = {Journal of automated reasoning}, volume = {27}, number = {4}, pages = {323--351}, doi = {10.1023/A:1011908113514}, ) @inproceedings(acl2, author = {M. Kaufmann and Strother Moore, J.}, year = {1996}, title = {ACL2: an industrial strength version of Nqthm}, booktitle = {Proceedings of 11th Annual Conference on Computer Assurance. COMPASS '96}, pages = {23--34}, doi = {10.1109/CMPASS.1996.507872}, ) @book(acl2-car, author = {Matt Kaufmann and Panagiotis Manolios and J Strother Moore}, year = {2000}, title = {Computer-Aided Reasoning: An Approach}, publisher = {Kluwer Academic Publishers}, doi = {10.1007/978-1-4615-4449-4}, ) @book(acl2-acs, author = {Matt Kaufmann and Panagiotis Manolios and J Strother Moore}, year = {2000}, title = {Computer-Aided Reasoning: Case Studies}, publisher = {Kluwer Academic Publishers}, doi = {10.1007/978-1-4757-3188-0}, ) @inproceedings(kaufmann-iteration-in-acl2, author = {Matt Kaufmann and J. Strother Moore}, year = {2020}, title = {Iteration in {ACL2}}, editor = {Grant O. Passmore and Ruben Gamboa}, booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2} Theorem Prover and its Applications}, series = {{EPTCS}}, volume = {327}, pages = {16--31}, doi = {10.4204/EPTCS.327.2}, ) @article(acl2-web, author = {Matt Kaufmann and J Strother Moore}, year = {2022}, title = {{ACL2 homepage}}, url = {https://www.cs.utexas.edu/users/moore/acl2/}, ) @inproceedings(manolios-framework-verifying-pipelined, author = {Panagiotis Manolios and Sudarshan K. Srinivasan}, year = {2005}, title = {Verification of executable pipelined machines with bit-level interfaces}, booktitle = {2005 International Conference on Computer-Aided Design, {ICCAD} 2005}, publisher = {{IEEE} Computer Society}, pages = {855--862}, doi = {10.1109/ICCAD.2005.1560182}, ) @article(manolios-framework-verifying-pipelined-journal, author = {Panagiotis Manolios and Sudarshan K. Srinivasan}, year = {2006}, title = {A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures}, journal = {J. Autom. Reason.}, volume = {37}, number = {1-2}, pages = {93--116}, doi = {10.1007/s10817-006-9035-0}, ) @inproceedings(ccg, author = {Panagiotis Manolios and Daron Vroon}, year = {2006}, title = {Termination Analysis with Calling Context Graphs}, editor = {Thomas Ball and Robert B. Jones}, booktitle = {Computer Aided Verification, 18th International Conference, {CAV}, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4144}, publisher = {Springer}, pages = {401--414}, doi = {10.1007/11817963\_36}, ) @inproceedings(manolios-termination-analysis, author = {Panagiotis Manolios and Daron Vroon}, year = {2006}, title = {Termination Analysis with Calling Context Graphs}, editor = {Thomas Ball and Robert B. Jones}, booktitle = {Computer Aided Verification, 18th International Conference Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4144}, publisher = {Springer}, pages = {401--414}, doi = {10.1007/11817963\_36}, ) @article(j-moore-acl2-milestones, author = {J. Strother Moore}, year = {2019}, title = {Milestones from the Pure Lisp Theorem Prover to ACL2}, journal = {Form. Asp. Comput.}, volume = {31}, number = {6}, pages = {699\IeC{\textendash}732}, doi = {10.1007/s00165-019-00490-3}, ) @inproceedings(moura-lean4, author = {Leonardo de Moura and Sebastian Ullrich}, year = {2021}, title = {The Lean 4 Theorem Prover and Programming Language}, editor = {Andr{\'{e}} Platzer and Geoff Sutcliffe}, booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on Automated Deduction, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12699}, publisher = {Springer}, pages = {625--635}, doi = {10.1007/978-3-030-79876-5\_37}, ) @inproceedings(z3, author = {Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj}, year = {2008}, title = {{Z3:} An Efficient {SMT} Solver}, editor = {C. R. Ramakrishnan and Jakob Rehof}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, {TACAS} 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2008, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4963}, publisher = {Springer}, pages = {337--340}, doi = {10.1007/978-3-540-78800-3\_24}, ) @inproceedings(passmore-verification-financial-algorithms, author = {Grant Olney Passmore and Denis Ignatovich}, year = {2017}, title = {Formal Verification of Financial Algorithms}, editor = {Leonardo de Moura}, booktitle = {Automated Deduction -- CADE 26}, publisher = {Springer International Publishing}, address = {Cham}, pages = {26--41}, doi = {10.1007/978-3-319-63046-5_3}, ) @inproceedings(peng-smtlink, author = {Yan Peng and Mark Greenstreet}, year = {2015}, title = {Extending ACL2 with SMT Solvers}, editor = {Matt Kaufmann and David L. Rager}, booktitle = {{\rm Proceedings Thirteenth International Workshop on the} ACL2 Theorem Prover and Its Applications}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {192}, publisher = {Open Publishing Association}, pages = {61--77}, doi = {10.4204/EPTCS.192.6}, ) @inproceedings(smtlink, author = {Yan Peng and Mark R. Greenstreet}, year = {2015}, title = {Extending {ACL2} with {SMT} Solvers}, editor = {Matt Kaufmann and David L. Rager}, booktitle = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem Prover and Its Applications}, series = {{EPTCS}}, volume = {192}, pages = {61--77}, doi = {10.4204/EPTCS.192.6}, ) @inproceedings(smtlink2, author = {Yan Peng and Mark R. Greenstreet}, year = {2018}, title = {Smtlink 2.0}, editor = {Shilpi Goel and Matt Kaufmann}, booktitle = {Proceedings of the 15th International Workshop on the {ACL2} Theorem Prover and Its Applications}, series = {{EPTCS}}, volume = {280}, pages = {143--160}, doi = {10.4204/EPTCS.280.11}, ) @phdthesis(rager-thesis, author = {David L. Rager}, year = {2012}, title = {Parallelizing an Interactive Theorem Prover: Functional Programming and Proofs with ACL2}, school = {The University of Texas at Austin}, ) @inproceedings(reeber-sulfa, author = {Erik Reeber and Warren A. Hunt Jr.}, year = {2006}, title = {A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in {ACL2} {(SULFA)}}, editor = {Ulrich Furbach and Natarajan Shankar}, booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR} , Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4130}, publisher = {Springer}, pages = {453--467}, doi = {10.1007/11814771\_38}, ) @article(russinoff-amd-proof, author = {David M Russinoff}, year = {1998}, title = {A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7\IeC{\texttrademark} processor}, journal = {LMS Journal of Computation and Mathematics}, volume = {1}, pages = {148--200}, doi = {10.1112/S1461157000000176}, ) @inproceedings(sawada-acl2six, author = {Jun Sawada and Erik Reeber}, year = {2006}, title = {{ACL2SIX:} {A} Hint used to Integrate a Theorem Prover and an Automated Verification Tool}, booktitle = {Formal Methods in Computer-Aided Design, 6th International Conference, Proceedings}, publisher = {{IEEE} Computer Society}, pages = {161--170}, doi = {10.1109/FMCAD.2006.3}, ) @inproceedings(swords-bit-blasting, author = {Sol Swords and Jared Davis}, year = {2011}, title = {Bit-Blasting {ACL2} Theorems}, editor = {David S. Hardin and Julien Schmaltz}, booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover and its Applications}, series = {{EPTCS}}, volume = {70}, pages = {84--102}, doi = {10.4204/EPTCS.70.7}, ) @article(reasoning-engine-preprint, author = {Andrew Walter and Seth Cooper and Panagiotis Manolios}, year = {2021}, title = {A Reasoning Engine for the Gamification of Loop-Invariant Discovery}, journal = {CoRR}, volume = {abs/2109.01121}, eprint = {2109.01121}, ) @article(idg, author = {Andrew T. Walter and Benjamin Boskin and Seth Cooper and Panagiotis Manolios}, year = {2019}, title = {Gamification of Loop-Invariant Discovery from Code}, journal = {Proceedings of the AAAI Conference on Human Computation and Crowdsourcing}, volume = {7}, number = {1}, pages = {188--196}, url = {https://ojs.aaai.org/index.php/HCOMP/article/view/5277}, ) @article(async-proof-processing, author = {Makarius Wenzel}, year = {2012}, title = {Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {285}, pages = {101--114}, doi = {10.1016/j.entcs.2012.06.009}, )