SPEN - A Solver for Separation Logic Entailments

SPEN - Rozhodovací procedura pro separační logiku

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

Lengál Ondřej, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Enea Constantin
Sighireanu Mihaela, prof. Ing., PhD.

program verification, decision procedures, separation logic, tree automata

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.

http://www.liafa.univ-paris-diderot.fr/spen/

Free software under the terms of GNU GPL (cf. http://www.gnu.org/licenses/gpl.html).

Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, start: 2014-01-01, end: 2016-12-31, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-12-31, completed

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)