Term Equivalence and Applications (TEA) Seminar

The TEA seminar is an online seminar between groups in Nijmegen, Amsterdam and Nagoya. We discuss methods to prove equivalence of term rewriting systems, or program equvialence using term rewriting systems.

Events:

• Tuesday 14 November, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Naoki Nishida
  Title: On Transforming C Programs with Pointers into LCTRSs with Separation Logic
  Abstract: In this talk, I introduce an idea of transforming C programs with pointers into LCTRSs with Separation Logic (SL-LCTRS). I first propose SL-LCTRSs used for modeling heaps in configurations of imperative programs. Then, referring to some inference rules of semantics, I show an example of transforming a small C program with pointers into an SL-LCTRS.
• Friday 28 April, 09:00 (Amsterdam/Nijmegen time) / 16:00 (Nagoya time)
  Speaker: Kasper Hagens
  Title: Matrix Invariants for program equivalence in LCTRSs
  Abstract: LCTRSs can be used as a formal language to prove program equivalence. A successful proof often requires the introduction of an invariant. We discuss a new method for automatically generating such invariants by using matrix calculations.
• Monday 20 March, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Misaki Kojima
  Title: From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
  Abstract: An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by a logically constrained term rewrite system to an all-path reachability problem of the system. In this talk, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.
• Tuesday 10 January, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Liye Guo and Cynthia Kop
  Title: Higher-order LCTRSs
  Abstract: In this presentation, Cynthia will first presents thoughts and considerations for designing a higher-order rewriting formalism that is both general enough to express the things we need, and practical to analyse. Following this introduction, Liye will present a concrete definition of an applicative higher-order extension of LCTRSs (with types, but without abstraction).
• Tuesday 22 November, 09:00 (Amsterdam/Nijmegen time) / 17:00 (Nagoya time)
  Speaker: Naoki Nishida
  Title: Equivalence Verification via Transformation of Programs into LCTRSs
  Abstract: In this talk, I first introduce my researches on constrained rewriting, together with an initial motivation (academic applications) and recent motivations (industrial applications). Then, I list LCTRS researches in the last decade: the proposal in 2013, an application to equivalence verification, Ctrl, and related work on LCTRSs, including on-going works in my group. Finally, I explain the progress of a common file format for LCTRSs, which is an on-going work of ARI project.