We describe defret-mutual-generate, a utility for proving ACL2 theorems ...
FGL is a successor to GL, a proof procedure for ACL2 that allows complic...
Verification of modern microprocessors is a complex task that requires a...
This paper describes a strategy for providing hints during an ACL2 proof...
We describe an effort to soundly use off-the-shelf incremental SAT solve...
share