Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

Release of the CTL and fairness provers described in the CADE'17 submission.

Gadi Tellez and James Brotherston
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

An archive containing executable binaries, test suite and source code is provided.

Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic

Release of the procedural termination prover described in the CPP'17 submission

Reuben N. S. Rowe and James Brotherston
Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic

A compressed archive containing the source code, test suite and Linux x64 binaries is below.
See cyclist-prover.org for more information.

Model checking for symbolic-heap separation logic with inductive predicates

Release of the model checker described in the POPL'16 submission

James Brotherston, Nikos Gorogiannis, Max Kanovich, and Reuben Rowe
Model checking for symbolic-heap separation logic with inductive predicates

A compressed archive containing the test suite and Linux x64 binaries is below.
See doc/README.POPL16 for more information.

Disproving Inductive Entailments in Separation Logic via Base Pair Approximation

Release of the tool and test suite described in the TABLEAUX15 submission:

James Brotherston and Nikos Gorogiannis.
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation

A pre-compiled version of the code can be found below.

Cyclic Abduction of Inductively Defined Safety and Termination Preconditions

Release of the tool and test suite described in the SAS14 submission:

James Brotherston and Nikos Gorogiannis.
Cyclic Abduction of Inductively Defined Safety and Termination Preconditions.

A link to a VirtualBox virtual machine loaded with a pre-compiled version of the software and the test suite will soon be posted here.

A satisfiability checker for separation logic with inductive predicates

Release of the checker described in the CSL-LICS14 submission:

James Brotherston, Carsten Fuhs, Nikos Gorogiannis, and Juan Navarro Perez.
A decision procedure for satisfiability in separation logic with inductive predicates.

Binaries (for a Linux x64 system) and a test suite are included in the slsat.tar.gz file. After downloading, look at README.CSL-LICS14 for instructions on how to run the tool and the test suite.