Abstract

In term rewriting, reachability analysis is concerned with the problem of deciding whether or not one term is reachable from another by rewriting. Reachability analysis has several applications in termination and confluence analysis of rewrite systems. We give a unified view on reachability analysis for rewriting with and without conditions by means of what we call reachability constraints. Moreover, we provide several techniques that fit into this general framework and can be efficiently implemented. Our experiments show that these techniques increase the power of existing termination and confluence tools.

BibTeX

@inproceedings{CSAY-TACAS19,
  author    = "Christian Sternagel and Akihisa Yamada",
  title     = "Reachability Analysis for Termination and Confluence of Rewriting",
  booktitle = "Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", 
  editor    = "Tomáš Vojnar and Lijun Zhang",
  series    = "Lecture Notes in Computer Science",
  volume    = 11427,
  pages     = "262--278",
  year      = 2019,
  doi       = "10.1007/978-3-030-17462-0_15"
}