SLIDE: Separation Logic with Inductive Definitions

SLIDE: Separační logika s induktivními definicemi

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

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

Separation logic, inductive definitions, entailment

SLIDE je prototypový nástroj určený k ověření incluze množiny modelů formulí popsaných Separační logikou s induktivními definicemi rekurzivních datových struktur (linkované listy, stromy, a složitější).

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

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)