A satisfiability checker for separation logic with inductive predicates
·
444 commits
to master
since this release
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.