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)
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).
Projects
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures (GA14-11384S)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Verification and Optimization of Computer Systems (FIT-S-12-1)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Verification and Optimization of Computer Systems (FIT-S-12-1)
Research groups
Departments