INCLUDER (tracer): Trace Inclusion for Data Word Automata

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

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

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

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

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.

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

Free software under the terms of GNU GPL (cf. http://www.gnu.org/licenses/gpl.html).

Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, 2014-2016, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, 2014-2016, completed
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)