You are here

Symbolic Reachability Analysis for Rewrite Theories


Camilo Rocha, Escuela Colombiana de Ingeniería, Colombia

Symbolic techniques that represent possibly infinite sets of states by symbolic constraints and support decision or semi-decision procedures based on such constraints have become essential to automate large parts of the verification of secure, trustworthy systems and make their verification much more scalable.  They include: (i) SAT solving and other decision procedures, and their combination into Satisfiability Modulo Theories (SMT) solvers; (ii) rewriting- and unification-based techniques, including rewriting modulo theories and narrowing modulo theories; and (iii) automata-based model checking techniques, which describe infinite sets of states and/or system traces symbolically by various kinds of automata.

The following topics will be addressed in this lecture:

  • rewriting modulo SMT, a general and extensible technique for symbolic analysis that combines the power of SMT solving and rewriting-based analysis
  • inductive reachability analysis for infinite state systems based on unification modulo equational theories and SMT solving


  • First-order logic
  • Equational deduction
  • Term rewriting systems
  • Rewriting logic (optional) 

All the slides can be accessed here: