References

  1. ESRAP – a packrat parser for Common Lisp. Available at https://github.com/scymtym/esrap. Accessed on April 25th, 2022.
  2. Hunchentoot – The Common Lisp web server formerly known as TBNL. Available at http://edicl.github.io/hunchentoot/. Accessed on April 25th, 2022.
  3. USOCKET – Universal socket library for Common Lisp. Available at https://usocket.common-lisp.dev/. Accessed on April 25th, 2022.
  4. Xtext. Available at https://www.eclipse.org/Xtext/. Accessed on April 25th, 2022.
  5. Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann & Panagiotis Manolios (2011): Integrating Testing and Interactive Theorem Proving. In: David S. Hardin & Julien Schmaltz: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, EPTCS 70, pp. 4–19, doi:10.4204/EPTCS.70.1.
  6. Harsh Raju Chamarthi, Peter C. Dillinger & Panagiotis Manolios (2014): Data Definitions in the ACL2 Sedan. In: Freek Verbeek & Julien Schmaltz: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, EPTCS 152, pp. 27–48, doi:10.4204/EPTCS.152.3.
  7. Jared Davis (2013): Embedding ACL2 models in end-user applications. In: Proc. of Do-Form'13, Do-Form. AISB, pp. 49–56.
  8. Peter Dillinger, Matt Kaufmann & Pete Manolios (2007): Hacking and Extending ACL2. In: Proceedings of the Seventh International Workshop on the ACL2 Theorem Prover and its Applications.
  9. Peter C. Dillinger, Panagiotis Manolios, Daron Vroon & J. Strother Moore (2007): ACL2s: ``The ACL2 Sedan''. Electronic Notes in Theoretical Computer Science 174(2), pp. 3–18, doi:10.1016/j.entcs.2006.09.018. Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006).
  10. Ruben A Gamboa & Matt Kaufmann (2001): Nonstandard analysis in ACL2. Journal of automated reasoning 27(4), pp. 323–351, doi:10.1023/A:1011908113514.
  11. M. Kaufmann & J. Strother Moore (1996): ACL2: an industrial strength version of Nqthm. In: Proceedings of 11th Annual Conference on Computer Assurance. COMPASS '96, pp. 23–34, doi:10.1109/CMPASS.1996.507872.
  12. Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, doi:10.1007/978-1-4615-4449-4.
  13. Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000): Computer-Aided Reasoning: Case Studies. Kluwer Academic Publishers, doi:10.1007/978-1-4757-3188-0.
  14. Matt Kaufmann & J. Strother Moore (2020): Iteration in ACL2. In: Grant O. Passmore & Ruben Gamboa: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, EPTCS 327, pp. 16–31, doi:10.4204/EPTCS.327.2.
  15. Matt Kaufmann & J Strother Moore (2022): ACL2 homepage. Available at https://www.cs.utexas.edu/users/moore/acl2/.
  16. Panagiotis Manolios & Sudarshan K. Srinivasan (2005): Verification of executable pipelined machines with bit-level interfaces. In: 2005 International Conference on Computer-Aided Design, ICCAD 2005. IEEE Computer Society, pp. 855–862, doi:10.1109/ICCAD.2005.1560182.
  17. Panagiotis Manolios & Sudarshan K. Srinivasan (2006): A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures. J. Autom. Reason. 37(1-2), pp. 93–116, doi:10.1007/s10817-006-9035-0.
  18. Panagiotis Manolios & Daron Vroon (2006): Termination Analysis with Calling Context Graphs. In: Thomas Ball & Robert B. Jones: Computer Aided Verification, 18th International Conference, CAV, Proceedings, Lecture Notes in Computer Science 4144. Springer, pp. 401–414, doi:10.1007/11817963_36.
  19. Panagiotis Manolios & Daron Vroon (2006): Termination Analysis with Calling Context Graphs. In: Thomas Ball & Robert B. Jones: Computer Aided Verification, 18th International Conference Proceedings, Lecture Notes in Computer Science 4144. Springer, pp. 401–414, doi:10.1007/11817963_36.
  20. J. Strother Moore (2019): Milestones from the Pure Lisp Theorem Prover to ACL2. Form. Asp. Comput. 31(6), pp. 699732, doi:10.1007/s00165-019-00490-3.
  21. Leonardo de Moura & Sebastian Ullrich (2021): The Lean 4 Theorem Prover and Programming Language. In: André Platzer & Geoff Sutcliffe: Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Proceedings, Lecture Notes in Computer Science 12699. Springer, pp. 625–635, doi:10.1007/978-3-030-79876-5_37.
  22. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: C. R. Ramakrishnan & Jakob Rehof: 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, Lecture Notes in Computer Science 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  23. Grant Olney Passmore & Denis Ignatovich (2017): Formal Verification of Financial Algorithms. In: Leonardo de Moura: Automated Deduction – CADE 26. Springer International Publishing, Cham, pp. 26–41, doi:10.1007/978-3-319-63046-5_3.
  24. Yan Peng & Mark Greenstreet (2015): Extending ACL2 with SMT Solvers. In: Matt Kaufmann & David L. Rager: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Electronic Proceedings in Theoretical Computer Science 192. Open Publishing Association, pp. 61–77, doi:10.4204/EPTCS.192.6.
  25. Yan Peng & Mark R. Greenstreet (2015): Extending ACL2 with SMT Solvers. In: Matt Kaufmann & David L. Rager: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, EPTCS 192, pp. 61–77, doi:10.4204/EPTCS.192.6.
  26. Yan Peng & Mark R. Greenstreet (2018): Smtlink 2.0. In: Shilpi Goel & Matt Kaufmann: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, EPTCS 280, pp. 143–160, doi:10.4204/EPTCS.280.11.
  27. David L. Rager (2012): Parallelizing an Interactive Theorem Prover: Functional Programming and Proofs with ACL2. The University of Texas at Austin.
  28. Erik Reeber & Warren A. Hunt Jr. (2006): A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning, Third International Joint Conference, IJCAR , Proceedings, Lecture Notes in Computer Science 4130. Springer, pp. 453–467, doi:10.1007/11814771_38.
  29. David M Russinoff (1998): A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7processor. LMS Journal of Computation and Mathematics 1, pp. 148–200, doi:10.1112/S1461157000000176.
  30. Jun Sawada & Erik Reeber (2006): ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool. In: Formal Methods in Computer-Aided Design, 6th International Conference, Proceedings. IEEE Computer Society, pp. 161–170, doi:10.1109/FMCAD.2006.3.
  31. Sol Swords & Jared Davis (2011): Bit-Blasting ACL2 Theorems. In: David S. Hardin & Julien Schmaltz: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, EPTCS 70, pp. 84–102, doi:10.4204/EPTCS.70.7.
  32. Andrew Walter, Seth Cooper & Panagiotis Manolios (2021): A Reasoning Engine for the Gamification of Loop-Invariant Discovery. CoRR abs/2109.01121. ArXiv:2109.01121.
  33. Andrew T. Walter, Benjamin Boskin, Seth Cooper & Panagiotis Manolios (2019): Gamification of Loop-Invariant Discovery from Code. Proceedings of the AAAI Conference on Human Computation and Crowdsourcing 7(1), pp. 188–196. Available at https://ojs.aaai.org/index.php/HCOMP/article/view/5277.
  34. Makarius Wenzel (2012): Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. Electronic Notes in Theoretical Computer Science 285, pp. 101–114, doi:10.1016/j.entcs.2012.06.009.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org