SPEN - A Solver for Separation Logic Entailments

SPEN - Rozhodovací procedura pro separační logiku

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Poskytovatel licence na výsledek nepožaduje licenční poplatek

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

program verification, decision procedures, separation logic, tree automata

Tento program obsahuje implementaci rozhodovací procedury pro fragment separační logiky navrženou ve článku: 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/

Volně šiřitelný software poskytovaný pod licencí GNU GPL (přesné znění licence je dostupné na stránce http://www.gnu.org/licenses/gpl.html).

Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, 2014-2016, ukončen
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, ukončen
Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, 2014-2016, ukončen
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, 2012-2014, ukončen

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Ústav inteligentních systémů (UITS)