research
∙
09/29/2020
Generating Mutually Inductive Theorems from Concise Descriptions
We describe defret-mutual-generate, a utility for proving ACL2 theorems ...
share
research
∙
09/29/2020
New Rewriter Features in FGL
FGL is a successor to GL, a proof procedure for ACL2 that allows complic...
research
∙
12/21/2019
Verifying x86 Instruction Implementations
Verification of modern microprocessors is a complex task that requires a...
research
∙
10/10/2018
Hint Orchestration Using ACL2's Simplifier
This paper describes a strategy for providing hints during an ACL2 proof...
research
∙
10/10/2018