Product Details
dWiNA - An Implementation of Decision Procedure for WS1S
Created: 2015
Czech title
dWiNA - Implementace rozhodovací procedury pro WS1S
Type
software
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
Authors
Fiedor Tomáš, Ing., Ph.D.
(RG VERIFIT)
Lengál Ondřej, Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Keywords
antichainsWS1Sfinite automatasubsumptionnondeterministic automata
Description
This tool is an implementation of novel approach based on anti-chains for deciding Weak Monadic Second-Order Logic of one successor (WS1S).
Location
Nástroj i dokumentaci lze získat na URL:http://www.fit.vutbr.cz/research/groups/verifit/tools/dWiNA/
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, 2014-2016, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, 2014-2016, completed
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed
Verification of Infinite State Systems Based on Finite Automata, GACR, Postdoktorandské granty, GP13-37876P, 2013-2015, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, 2014-2016, completed
The IT4Innovations Centre of Excellence, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, 2011-2015, completed
Verification of Infinite State Systems Based on Finite Automata, GACR, Postdoktorandské granty, GP13-37876P, 2013-2015, completed
Research groups
Departments