dWiNA - An Implementation of Decision Procedure for WS1S

Název česky

dWiNA - Implementace rozhodovací procedury pro WS1S

Typ

software

Licence

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Licenční poplatek

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Autoři

Fiedor Tomáš, Ing., Ph.D. (VZ VERIFIT)
Lengál Ondřej, Ing., Ph.D. (UITS)
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)

Klíčová slova

antichains

WS1S

finite automata

subsumption

nondeterministic automata

Popis

Tento nástroj je implementací nového přístupu založeného na proti-řetězcích pro rozhodování slabé monadické druhořadé logiky s jedním následníkem (WS1S).

Umístění

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

Licenční podmínky

Volně šiřitelný software poskytovaný pod licencí GNU GPL (přesné znění licence je dostupné na stránce http://www.gnu.org/licenses/gpl.html).

Projekty

Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Verifikace nekonečně stavových systémů založená na konečných automatech, GAČR, Postdoktorandské granty, GP13-37876P, zahájení: 2013-02-01, ukončení: 2015-12-31, ukončen

Výzkumné skupiny

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Pracoviště

Ústav inteligentních systémů (UITS)