4 papers · 1 filter
Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications
Rob Sumners, Cuong Chau
This volume contains a selection of papers presented at the 17th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2022). The workshops are the premier t…
Computing and Proving Well-founded Orderings through Finite Abstractions
Rob Sumners
A common technique for checking properties of complex state machines is to build a finite abstraction then check the property on the abstract system -- where a passing check on the…
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…
Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications
Rob Sumners
We present a series of definitions and theorems demonstrating how to reduce the requirements for proving system refinements ensuring containment of fair stuttering runs. A primary…