SLIDE: Separation Logic with Inductive Definitions

Typ

software

Jazyk

anglicky

Autoři

Rogalewicz Adam, doc. Mgr., Ph.D., UITS (FIT)
Radu Iosif
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)

Popis

SLIDE is a prototype tool for checking entailment in Separation Logicwith user-provided inductive definitions of recursive data structures (lists, trees, and beyond)Basic features:

Sound and complete for local data structures (doubly-linked lists, trees with parent pointers, etc.)
Sound for non-local data structures (trees with linked leaves, skip-lists, etc. )
Built on top of the VATA tree automata library.

Klíčová slova

Separation logic, inductive definitions, entailment

Umístění

Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/

Licence

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

Licenční poplatek

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

Licenční podmínky

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í, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen

Výzkumné skupiny

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

Pracoviště

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