3 papers
cs.LO2020
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…
cs.LO2019
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…
cs.LO2017
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…