Prof. Ing. Tomáš Vojnar, Ph.D.

Gaston - Symbolic WS1S Solver

Authors:Fiedor Tomáš, Holík Lukáš, Janků Petr, Lengál Ondřej, Vojnar Tomáš
Type:software
Created:2017
Licence:required - no fee
Keywords:
WS1S
finite automata
logic
antichains
lazy evaluation
subsumption
monadic second-order logic
Description:
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.
Location:
The tool and manual is located at http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/ and at https://github.com/tfiedor/gaston
Research groups:
Departments:
Licence terms:
Free software under the terms of GNU GPL (cf.http://www.gnu.org/licenses/gpl.html).

Your IPv4 address: 54.163.209.109
Switch to IPv6 connection

DNSSEC [dnssec]