Detail produktu
INCLUDER (TRACER): Trace Inclusion for Data Word Automata
Vznik: 2015
Název česky
INCLUDER (tracer): Nástroj pro rozhodování běhové inkluze pro automaty nad daty
Typ
software
Licence
vyžadována - zdarma
Autoři
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Popis
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.
Umístění
Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/
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)
Centrum excelence IT4Innovations (ED1.1.00/02.0070)
Spolehlivost a bezpečnost v IT (FIT-S-14-2486)
Výzkumné skupiny
Pracoviště