Product detail

INCLUDER (tracer): Trace Inclusion for Data Word Automata

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

Product type

software

Abstract

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.

Keywords

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

Create date

1. 3. 2015

Location

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

Possibilities of use

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Licence fee

Poskytovatel licence na výsledek nepožaduje licenční poplatek

www

https://www.fit.vut.cz/research/product/422/