Product Details

INCLUDER (TRACER): Trace Inclusion for Data Word Automata

Created: 2015

Czech title
INCLUDER (tracer): Nástroj pro rozhodování běhové inkluze pro automaty nad daty
Type
software
License
required - free
Authors
Keywords

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

Description

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.

Location

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

Licence

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

Back to top