Cyclist

Cyclist is a generic, cyclic theorem prover framework written in OCaml and C++.

It can be used for constructing theorem provers over logics with inductive definitions. Existing instantiations include fragments of separation logic, and Hoare-style program logics for termination and/or safety.

A website dedicated to Cyclist and the various tools implemented within can be found at www.cyclist-prover.org. Included are instructions for use and building, as well as a live demo of the separation logic prover.

The source code for Cyclist is now hosted on GitHub and accessible from this repository.