ISR 2024 – Track C
Tools in Rewriting
Lecturer
Nao Hirokawa Japan Advanced Institute of Science and Technology
Course Description
Software tools based on rewriting have widely been used in the areas of programming languages, automated deduction, and software verification. The aim of this course is to give an introduction to rewriting tools and their tool developments. We study their usage, underlying theories, and potential applications, giving a brief introduction to related tool competitions (such as REC, termCOMP, CoCo, and CASC) and standard formats.
We pick up the following four types of tools.
-
Rewrite engines: After a brief introduction to algebraic specification
languages (CafeOBJ/Maude), we discuss theory of rewriting modulo
theories and implementation techniques for (AC) rewriting.
slides 4-up -
Termination: We study the dependency pair method with interpretation
orders for termination and runtime complexity analysis, discussing their
easy SMT encodings. We also briefly discuss how programs are translated
to rewrite systems.
slides 4-up -
Confluence: Rule labeling and transformation/decomposition techniques are
popular powerful methods in modern confluence tools. We study their
background theories and automation techniques, discussing translation
techniques from conditional rewrite systems to unconditional rewrite
systems.
slides 4-up -
Completion: Knuth–Bendix completion and ordered completion are
theoretical foundations for automatic theorem provers. We study basics of
these methods as well as recent techniques for finding suitable reduction
orders by MaxSAT. In addition, we discuss the split-if translation that
reduces the satisfiability problem of Horn clauses to a word problem.
slides 4-up
Prerequisites
Basis knowledge about rewriting, algebras, recursive path orders, and critical pairs.