Formalization and Execution of STE in HOL (Extended Version)

Abstract

We present an implementation of STE model checking in the higher-order logic theorem prover HOL. The motivation for such an implementation is to have an open source framework in which we can exploit the strengths of STE model checking and HOL theorem proving. We intend to use this framework for future experiments in the design and implementation of abstraction and reduction techniques to extend the reach of STE model checking. We show in this implementation how a deep embedding of STE in HOL allows us to reason about the STE verification results. By virtue of using HOL, we also have the possibility to prove that the abstraction and reduction techniques are sound.