Detail produktu
SPEN - A Solver for Separation Logic Entailments
Vznik: 2014
Název česky
SPEN - Rozhodovací procedura pro separační logiku
Typ
software
Licence
vyžadována - zdarma
Autoři
Enea Constantin (LIAFA UP7/CNRS)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Sighireanu Mihaela (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Sighireanu Mihaela (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Popis
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.
Umístění
Licence
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).
Projekty
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí (GA14-11384S)
Centrum excelence IT4Innovations (ED1.1.00/02.0070)
Spolehlivost a bezpečnost v IT (FIT-S-14-2486)
Verifikace a optimalizace počítačových systémů (FIT-S-12-1)
Centrum excelence IT4Innovations (ED1.1.00/02.0070)
Spolehlivost a bezpečnost v IT (FIT-S-14-2486)
Verifikace a optimalizace počítačových systémů (FIT-S-12-1)
Výzkumné skupiny
Pracoviště