Detail produktu

INCLUDER (tracer): Trace Inclusion for Data Word Automata

ROGALEWICZ, A. IOSIF, R. VOJNAR, T.

Typ produktu

software

Abstrakt

INCLUDER is a prototype implementation of our original decision procedure for data word automata. The procedure is based on combination of predicate abstraction, interpolation and CEGAR. The tool is build over the MathSat SMT solver.

Klíčová slova

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

Datum vzniku

1. 3. 2015

Umístění

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

Možnosti využití

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