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
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
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).
Projects
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures (GA14-11384S)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Reliability and Security in IT (FIT-S-14-2486)
The IT4Innovations Centre of Excellence (ED1.1.00/02.0070)
Research groups
Departments