INCLUDER (tracer): Trace Inclusion for Data Word Automata

INCLUDER (tracer): Nástroj pro rozhodování běhové inkluze pro automaty nad daty

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)

trace inclusion, data word automata, CEGAR, predicate abstraction, interpolation

INCLUDER představuje prototypovou implementaci naší techniky pro rozhodování běhové inkluze (trace inclusion) nad automaty s daty. Technika je založena na predikátové abstrakci, interpolaci a CEGAR smyčce. Implementace využívá MathSat SMT solver.

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

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

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

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