Gaston - Symbolic WS1S Solver
Gaston - Symbolická WS1S Rozhodovací Procedura
required - free
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.
The tool and manual is located at http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/ and at https://github.com/tfiedor/gaston
Free software under the terms of GNU GPL (cf.http://www.gnu.org/licenses/gpl.html).