106 citations · 294 across the 14 of their papers we have counts for
15 papers
Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications
Alessandro Coglio, Sol Swords
This volume contains the proceedings of the Eighteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2023), a two-day workshop held at the University…
Generating Mutually Inductive Theorems from Concise Descriptions
Sol Swords
We describe defret-mutual-generate, a utility for proving ACL2 theorems about large mutually recursive cliques of functions. This builds on previous tools such as defret-mutual and…
New Rewriter Features in FGL
Sol Swords
FGL is a successor to GL, a proof procedure for ACL2 that allows complicated finitary conjectures to be translated into efficient Boolean function representations and proved using…
Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners +1
Verification of modern microprocessors is a complex task that requires a substantial allocation of resources. Despite significant progress in formal verification, the goal of compl…
Hint Orchestration Using ACL2's Simplifier
Sol Swords
This paper describes a strategy for providing hints during an ACL2 proof, implemented in a utility called use-termhint. An extra literal is added to the goal clause and simplified…
Incremental SAT Library Integration Using Abstract Stobjs
Sol Swords
We describe an effort to soundly use off-the-shelf incremental SAT solvers within ACL2 by modeling the behavior of a SAT solver library as an abstract stobj. The interface allows A…