Gaston - Symbolic WS1S Solver

Gaston - Symbolická WS1S Rozhodovací Procedura

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

Fiedor Tomáš, Ing., Ph.D. (RG VERIFIT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Janků Petr, Ing. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)

WS1S finite automata logic antichains lazy evaluation subsumption monadic second-order logic

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.

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

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

Bezpečné a spolehlivé počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, completed
Efficient Automata for Formal Reasoning, GACR, Juniorské granty, GJ16-24707Y, 2016-2018, running
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, completed
Relaxed equivalence checking for approximate computing, GACR, Standardní projekty, GA16-17538S, 2016-2018, running

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)