Přístupnostní navigace
E-application
Search Search Close
Product detail
FIEDOR, T. HOLÍK, L. JANKŮ, P. LENGÁL, O. VOJNAR, T.
Product type
software
Abstract
Gaston is an implementation of backward decision procedure for WS1S logic (weak second-order theory of k successors). The tool is using libmona a highly optimised deterministic finite tree automata library that supports semi-symbolic encoding using multi-terminal binary decision diagrams (MTBDDs) for storing transition table of the automaton. Procedure generates state space on-the-fly and prunes the states using the antichain-based approach. The tool works on the symbolical representation of the formula as Symbolic Automata and tries to prove on-the-fly that the initial states intersect the final states to (dis)prove validity.
Keywords
WS1S finite automata logic antichains lazy evaluation subsumption monadic second-order logic
Create date
4. 2. 2017
Location
Nástroj a dodatečné informace se nacházejí na http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/ a https://github.com/tfiedor/gaston
Possibilities of use
K využití výsledku jiným subjektem je vždy nutné nabytí licence
Licence fee
Poskytovatel licence na výsledek nepožaduje licenční poplatek
www
https://www.fit.vut.cz/research/product/511/