Constrained Rewriting and SMT: Emerging Trends in Rewriting

This is a joint project between Austria and Japan. It involves research teams from the following universities:

  • Hokkaido University
  • Japan Advanced Institute of Science and Technology
  • Nagoya University
  • University of Innsbruck
  • University of Yamanashi
  • Vienna University of Technology

The project deals with the following five tasks:

  • Constrained Rewriting
  • SMT (Satisfiability Modulo Theories)
  • Completion
  • Complexity
  • Certification

The overall aim is to advance applicability of rewriting techniques in verification by focusing on constrained rewriting, a paradigm that suits program analysis better than unconstrained rewriting. Constrained rewriting is a well-studied area but different notions of constrained rewriting exist and only few attempts for automation have been undertaken. Hence a thorough comparison of these approaches is non-trivial. In this project we want to make these approaches comparable, e.g., by a suitable competition of dedicated tools. Nowadays many rewriting tools use so-called SMT solvers as external software to solve (extended) boolean constraints. The second aim of the project is to make (existing) rewriting tools more powerful by extending the underlying SMT solvers with direct support for constrained rewriting. SMT solvers are also essential for some variants and extensions of (Knuth-Bendix) completion which are studied in task 3. The aim of task 4 is to establish upper bounds on the complexity of programs automatically; also here the achievements of tasks 1 and 2 are essential for success. Finally, task 5 addresses to establish soundness of the aforementioned approaches mechanically, i.e., tool (output) is verified automatically with the help of a theorem prover.


The project is coordinated by

  • Aart Middeldorp (coordinator Austria)
  • Masahiko Sakai (coordinator Japan)

The Innsbruck team consists of

  • Cynthia Kop
  • Aart Middeldorp
  • Georg Moser
  • Thomas Sternagel
  • René Thiemann
  • Sarah Winkler
  • Harald Zankl

The Vienna team consists of

  • Karl Gmeiner
  • Bernhard Gramlich



  • Kickoff meeting, July 2 – 6, 2012, Gamagori, Japan
  • 39th TRS meeting, September 18 – 20, 2013, Akita, Japan
  • 41st TRS meeting, September 26 – 28, 2014, Sapporo, Japan
FWF “International Cooperation Project” project number

I 963-N15


Nach oben scrollen