Skip to content

Model checking for symbolic-heap separation logic with inductive predicates

Choose a tag to compare

@ngorogiannis ngorogiannis released this 18 Nov 13:52

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.