Product Details
Gaston - Symbolic WS1S Solver
Created: 2017
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Janků Petr, Ing. (FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
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.
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).
IT4Innovations excellence in science (LQ1602)
Relaxed equivalence checking for approximate computing (GA16-17538S)
Secure and Reliable Computer Systems (FIT-S-17-4014)