Result Details

dWiNA - An Implementation of Decision Procedure for WS1S

Created: 2015
Type
software
Language
English
Authors
Fiedor Tomáš, Ing., Ph.D., DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D.
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Description

This tool is an implementation of novel approach based on anti-chains for deciding Weak Monadic Second-Order Logic of one successor (WS1S).

Keywords
antichains
WS1S
finite automata
subsumption
nondeterministic automata
Location

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

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 GPL (cf.http://www.gnu.org/licenses/gpl.html).

Projects
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, start: 2014-01-01, end: 2016-12-31, completed
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed
Verification of Infinite State Systems Based on Finite Automata, GACR, Postdoktorandské granty, GP13-37876P, start: 2013-02-01, end: 2015-12-31, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top