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. (RG VERIFIT)
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, start: 2017-03-01, end: 2020-02-29, completed
Efficient Automata for Formal Reasoning, GACR, Juniorské granty, GJ16-24707Y, start: 2016-01-01, end: 2018-12-31, running
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, start: 2016-01-01, end: 2020-12-31, completed
Relaxed equivalence checking for approximate computing, GACR, Standardní projekty, GA16-17538S, start: 2016-01-01, end: 2018-12-31, running

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

Department of Intelligent Systems (DITS)