Product Details
SPEN - A Solver for Separation Logic Entailments
Created: 2014
Czech title
SPEN - Rozhodovací procedura pro separační logiku
Type
software
License
In order to use the result by another entity, it is always necessary to acquire a license
License Fee
The licensor does not require a license fee for the result
Authors
Lengál Ondřej, Ing., Ph.D.
(DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Enea Constantin (FIT)
Sighireanu Mihaela
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Enea Constantin (FIT)
Sighireanu Mihaela
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.
Location
License Conditions
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, GACR, Standardní projekty, GA14-11384S, 2014-2016, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, 2014-2016, completed
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, 2012-2014, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, 2014-2016, completed
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, 2012-2014, completed
Research groups
Departments