swMATH ID: 10115
Software Authors: Waldmann, J.
Description: Matchbox: A tool for match-bounded string rewriting. The program Matchbox implements the exact computation of the set of descendants of a regular language, and of the set of non-terminating strings, with respect to an (inverse) match-bounded string rewriting system. Matchbox can search for proof or disproof of a Boolean combination of match-height properties of a given rewrite system, and some of its transformed variants. This is applied in various ways to search for proofs of termination and non-termination. Matchbox is the first program that delivers automated proofs of termination for some difficult string rewriting systems.
Homepage: http://link.springer.com/chapter/10.1007/978-3-540-25979-4_6
Source Code:  https://github.com/jwaldmann/matchbox/
Related Software: AProVE; Tyrolean; Haskell; TORPA; CiME; Jambox; MU-TERM; CeTA; Isabelle/HOL; TPA; TPDB; Maude; OBJ3; CoLoR; MiniSat; Chaff; Tsukuba; term-rewriting; GitHub; SeaHorn
Cited in: 23 Publications

Citations by Year