Faculty of Information Technology, BUT

Product Details

SPEN - A Solver for Separation Logic Entailments

Created: 2014

Czech title
SPEN - Rozhodovací procedura pro separační logiku
Type
software
License
required - free
Authors
Enea Constantin (LIAFA UP7/CNRS)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Sighireanu Mihaela (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords
program verification, decision procedures, separation logic, tree automata
Description
This program provides an implementation of a decision procedure for a fragment of separation logic proposed in the paper: C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. In Proc. of 12th Asian Symposium on Programming Languages and Systems---APLAS'14, Singapore, 2014, volume 8858 of LNCS, pages 314--333, 2014. Springer-Verlag.
Licence
Free software under the terms of GNU GPL (cf. http://www.gnu.org/licenses/gpl.html).
Back to top