Holfoot

Description

Holfoot is an implementation of Smallfoot inside the HOL 4 theorem prover. In addition to the features supported by Smallfoot it can handle data and supports interactive proofs. Moreover, it can handle arrays. It is described in detail in my dissertation.

Simple specifications with data like copying a list can be handled automatically. More complicated ones like fully functional specifications of filtering a list, mergesort, quicksort or an implementation of red-black trees require user interaction. During this interaction all the features of the HOL 4 theorem prover can be used, including the interface to external SMT solvers like Yices.

HOL 4 is needed to run Holfoot interactively. For purely automated useage precompiled command-line versions are available.

Downloads

Web-Interface

Documentation