research
∙
09/29/2020
Iteration in ACL2
Iterative algorithms are traditionally expressed in ACL2 using recursion...
share
research
∙
10/10/2018
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)
We present a tool that automates termination proofs for recursive defini...
research
∙
10/09/2018
Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications
This volume contains the proceedings of the Fifteenth International Work...
research
∙
05/03/2017
A Versatile, Sound Tool for Simplifying Definitions
We present a tool, simplify-defun, that transforms the definition of a g...
research
∙
09/18/2015
Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications
This volume contains the proceedings of the Thirteenth International Wor...
research
∙
06/06/2014
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
We report on improvements to ACL2 made since the 2013 ACL2 Workshop....
research
∙
04/30/2013
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1
We report on highlights of the ACL2 enhancements introduced in ACL2 rele...
research
∙
05/23/2011