Stefan Ciobaca

Reachability in Logically Constrained Term Rewriting Systems

Ștefan Ciobâcă (Alexandru Ioan Cuza University, Romania)

Find lecture notes here.

Lately there has been significant interest in combining term rewriting and SMT solving, motivated by applications in verification.

In this lecture, I will introduce logically constrained term rewriting systems (LCTRSs). LCTRSs combine term rewriting with builtins and constraints, which are solved using SMT. LCTRSs generalize well known extensions of TRSs, such as Integer TRSs, by making the builtins (e.g., integers) parametric. I will introduce a method for proving reachability in LCTRSs for both a bounded and an unbounded number of steps. The lecture includes a number of exercises in modelling systems as LCTRSs and proving reachability properties of the respective LCTRSs using the RMT tool (github.com/ciobaca/rmt/).

Outline of the lecture

  • Logically Constrained Term Rewriting Systems (LCTRSs) – theory and small exercises;
  • Proving Reachability Properties in LCTRSs – theory and small exercises;
  • Practical Experiments in Proving Reachability Properties – using the RMT tool.

Exercises or experiments

The lecture includes both a few theoretical exercises, as well as practical experiments using the RMT tool (github.com/ciobaca/rmt/).
For the practical part, students need to have a reasonably recent Linux/MacOSX/Windows computer with an SMT solver (Z3 or CVC4) installed. I will provide RMT binaries for the three platforms, or alternatively the students can very easily compile it from source with a reasonably recent C++ compiler (gcc, clang/llvm, Visual Studio). There is also a Web interface to RMT, but the experience would be suboptimal.

Bibliographical references

The main bibliographical references for the lecture would be:

  1. Stefan Ciobaca and Dorel Lucanu. A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. IJCAR 2018;
  2. Stefan Ciobaca, Andrei Arusoaie, and Dorel Lucanu. Unification Modulo Builtins. WoLLIC 2018.

Some additional relevant material (using ASCII characters for readability) is:

  1. Luis Aguirre, Narciso Mart-Oliet, Miguel Palomino, and Isabel Pita. Conditional Narrowing Modulo SMT and Axioms. PPDP 2017;
  2. Kyungmin Bae and Camilo Rocha. Guarded Terms for Rewriting Modulo SMT. FACS 2017;
  3. Claude Kirchner, Helene Kirchner, and Michael Rusinowitch. Deduction with Symbolic Constraints. Technical Report RR-1358, INRIA, 1990;
  4. Cynthia Kop. Termination of LCTRSs. CoRR, abs/1601.03206, 2016;
  5. Cynthia Kop and Naoki Nishida. Term Rewriting with Logical Constraints.FroCoS 2013;
  6. Cynthia Kop and Naoki Nishida. Constrained Term Rewriting tooL. LPAR2015;
  7. Camilo Rocha, Jose Meseguer, and Cesar A. Munoz. Rewriting modulo SMT and open system analysis. J. Log. Algebr. Meth. Program., 86(1):269–297, 2017;
  8. Stephen Skeirik, Andrei Stefanescu, and Jose Meseguer. A constructor-based reach-ability logic for rewrite theories. TR. http://hdl.handle.net/2142/95770.

Comments are closed.