Matchbox

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.


References in zbMATH (referenced in 20 articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Hogg, Jonathan; Scott, Jennifer: On the use of suboptimal matchings for scaling and ordering sparse symmetric matrices. (2015)
  2. Korp, Martin; Middeldorp, Aart: Match-bounds revisited (2009)
  3. Payet, Étienne; Spoto, Fausto: Experiments with non-termination analysis for Java bytecode (2009)
  4. Thiemann, René; Sternagel, Christian: Certification of termination proofs using CeTA (2009)
  5. Zankl, Harald; Middeldorp, Aart: Increasing interpretations (2009)
  6. Zankl, Harald; Sternagel, Christian; Middeldorp, Aart: Transforming SAT into termination of rewriting (2009)
  7. Korp, Martin; Middeldorp, Aart: Match-bounds with dependency pairs for proving termination of rewrite systems (2008)
  8. Lucas, Salvador; Meseguer, José: Termination of just/fair computations in term rewriting (2008)
  9. Payet, Étienne: Loop detection in term rewriting using the eliminating unfoldings (2008)
  10. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: On tree automata that certify termination of left-linear term rewriting systems (2007)
  11. Hirokawa, Nao; Middeldorp, Aart: Tyrolean termination tool: techniques and features (2007)
  12. Waldmann, Johannes: Weighted automata for proving termination of string rewriting (2007)
  13. Endrullis, Jörg; Waldmann, Johannes; Zantema, Hans: Matrix interpretations for proving termination of term rewriting (2006)
  14. Hofbauer, Dieter; Waldmann, Johannes: Termination of string rewriting with matrix interpretations (2006)
  15. Lucas, Salvador: Proving termination of context-sensitive rewriting by transformation (2006)
  16. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes: Termination proofs for string rewriting systems via inverse match-bounds (2005)
  17. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: Finding finite automata that certify termination of string rewriting (2005)
  18. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: On tree automata that certify termination of left-linear term rewriting systems (2005)
  19. Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter: Proving and disproving termination of higher-order functions (2005)
  20. Zantema, H.: Termination of string rewriting proved automatically (2005)