Product detail

Gaston - Symbolic WS1S Solver

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

04.02.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

www