The Cyclist Framework and Provers

Cyclist is two things:

A generic, cyclic theorem prover framework. It can be used for constructing theorem provers that employ cyclic proof (usually, in order to treat inductively defined predicates) for practically any logic.
A collection of theorem provers and other tools, with a focus on Separation Logic with inductive definitions, hereafter abbreviated as SL. Checkout the demo for a live demonstration of the sl_prove tool.

Cyclist is written in OCaml and C++.

Actively maintained tools in Cyclist

sl_prove is a prover for entailments in SL. See the demo for a live demonstration.
sl_satcheck implements a decision procedure for satisfiability of SL formulas.
sl_disprove is a heuristic for disproving entailments in SL.
sl_modelcheck decides whether the given SL formula is satisfied by a provided program state.
while_prove is termination and/or safety prover for simple while-programs with pointers and dynamic allocation specified by SL formulas.
procedure_prove is a termination and/or safety prover for procedural imperative programs, where procedures are specified with pre- and postconditions composed of SL formulas.
while_abduce is a prover like while_prove, but which attempts to infer a suitable precondition in SL such that the target program will terminate/execute safely, including inferring the inductive definitions themselves.
fo_prove: A cyclic prover for (for all-exists) first order logic with inductive definitions.

goto_prove: A cyclic prover for a program logic like while_prove above, but for a go-to language.