Applied result detail

INCLUDER (TRACER): Trace Inclusion for Data Word Automata

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

Original Title

INCLUDER (TRACER): Trace Inclusion for Data Word Automata

English Title

INCLUDER (TRACER): Trace Inclusion for Data Word Automata

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.

Abstract in English

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

Key words in English

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

Location

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

Licence fee

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

www

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