Applied result detail

SPEN - A Solver for Separation Logic Entailments

LENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M.

Original Title

SPEN - A Solver for Separation Logic Entailments

English Title

SPEN - A Solver for Separation Logic Entailments

Type

Software

Abstract

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.

Abstract in English

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.

Keywords

program verification, decision procedures, separation logic, tree automata

Key words in English

program verification, decision procedures, separation logic, tree automata

Location

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

Licence fee

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

www

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