TR16-01 (2016) – RMT: Proving Reachability Properties in Constrained Term Rewriting Systems Modulo Theories

Stefan Ciobaca, Dorel Lucanu

We introduce the {\tt RMT} tool, which takes as input a constrained term rewriting system $\R$ and proves reachability properties of the form $\forall \tilde{x}.(c_1(\tilde{x}) \rightarrow \exists \tilde{y}.(c_2(\tilde{x}, \tilde{y}) \land t_1(\tilde{x}) \goesall_\R^* t_2(\tilde{x}, \tilde{y})))$, where $c_1, c_2$ are constraints over the variables $\tilde{x}$ and respectively $\tilde{x} \cup \tilde{y}$ and $t_1, t_2$ are terms over the variables $\tilde{x}$ and respectively $\tilde{x} \cup \tilde{y}$. By the relation $\goesall_\R^*$, we mean that $t_2(\tilde{x}, \tilde{y})$ is reachable across all paths in $\R$ starting in $t_1(\tilde{x})$. The reachability guarantee is sound for terminating paths starting in instances of $t_1(\tilde{x})$ and it was initially motivated by proving partial correctness of programs. The constrained term rewriting system is allowed to contain both interpreted and uninterpreted function symbols. The interpreted symbols are part of a theory that is a parameter to our tool and all rewriting steps are defined \emph{modulo} this theory. In practice, the interpreted symbols are handled by relying on an SMT solver.

Bibtex

@TechReport{rmt,
author = "\c{S}tefan Ciob^ac\u{a} and Dorel Lucanu",
title = {{RMT: Proving Reachability Properties in Constrained Term Rewriting Systems Modulo Theories}},
institution = "``Al.I.Cuza'' University of Ia{\c s}i,
                 Faculty of Computer Science",
year = "2016",
number = "TR 16-01",
note = "url{http://www.infoiasi.ro/~tr/tr.pl.cgi}"
}