Advances in ACL2 Proof Debugging Tools

Matt Kaufmann
(UT Austin, retired) 		J Strother Moore
(UT Austin, retired)

The experience of an ACL2 user generally includes many failed proof attempts. A key to successful use of the ACL2 prover is the effective use of tools to debug those failures. We focus on changes made after ACL2 Version 8.5: the improved break-rewrite utility and the new utility, with-brr-data.

In Alessandro Coglio and Sol Swords: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2023), Austin, TX, USA and online, November 13-14, 2023, Electronic Proceedings in Theoretical Computer Science 393, pp. 67–81.
Published: 14th November 2023.
ArXived at: https://dx.doi.org/10.4204/EPTCS.393.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org