Result Details

FLATA

Created: 2009
Type
software
Language
English
Authors
Konečný Filip, Ing., Ph.D., FIT (FIT), DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Bozga Marius
Radu Iosif
Description

FLATA is a toolset for the manipulation and the analysis of non-deterministic integer programs (also known as counter automata). FLATA checks emptiness of the model and transforms the input model to a smaller model with equivalent emptiness problem.

Keywords

counter automata, model checking, reachability analysis, emptiness problem

URL
License
In order to use the result by another entity, it is always necessary to acquire a license
License Fee
The licensor does not require a license fee for the result
License Conditions

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

Projects
Advanced Formal Approaches in the Design and Verification of Computer-Based Systems, GACR, Standardní projekty, GA102/07/0322, start: 2007-01-01, end: 2009-12-31, completed
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit, MŠMT, COST, OC10009, start: 2010-01-01, end: 2012-12-31, running
Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems, GACR, Doktorské granty, GD102/09/H042, start: 2009-01-30, end: 2012-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top