TERESE meeting Eindhoven, Friday, June 17, 2011

This meeting on term rewriting will be held at the Technische Universiteit Eindhoven (TU/e) on Friday, June 17, 2011, in the building

Hoofdgebouw, room 6.96 , building HG on campus map

How to reach?

Schedule:

time	speaker	title
13.30 - 14.15	Fausto Spoto (Verona, Italy and RWTH Aachen)	Julia: a Java Bytecode Static Analysis Tool
14.15 - 15.00	Vincent van Oostrom (UU)	Triangulation
15.00 - 15.30	break
15.30 - 16.15	Cynthia Kop (VU)	Transposing Termination Properties in Higher Order Rewriting
16.15 - 17.00	Matthias Raffelsieper (TU/e)	Productivity of Non-Orthogonal Term Rewrite Systems
17.00 - 17.30	TERESE business meeting
17.30 - ???	dinner in Tapas restaurant Si Senor, Dommelstraat 17

Abstracts:

Fausto Spoto: Julia: a Java Bytecode Static Analysis Tool
In this talk I will present the Julia static analysis for Java bytecode, describing its structure and available analyses. I will spend more time on its component for termination analysis. The conclusion will present challenges and possible solutions for the automatic analysis or large real software, in particular Android programs.

Vincent van Oostrom: Triangulation
Completion turns a rewrite relation into a confluent one while preserving termination. It does so by adjoining for pairs of critically diverging steps, say from a to both b and c, a step between the normal forms of b and c.
Triangulation, introduced here, proceeds in the same way but without taking normal forms first, directly adjoining a step between b and c instead. We show that triangulation turns any rewrite relation ->1 into a confluent rewrite relation ->, and that -> is terminating if ->1 is terminating and codeterministic:
(1) if b ->1 a and c ->1 a then b = c.
For steps ->2 adjoined to ->1 to yield ->, the following triangle property holds by definition of triangulation:
(2) if b ->2 c then there exists a with a -> b and a -> c
This leads to the question whether one may conclude to termination of the union -> of ->1 and ->2, just on the basis of termination of ->1 and ->2 and properties (1) and (2) alone. We provide answers to this and several fascinating related questions.
Joint work with Hans Zantema

Cynthia Kop: Transposing Termination Properties in Higher Order Rewriting
In higher order term rewriting, distinguished from first order term rewriting by the presence of bound variables and often also a type discipline, a plethora of different frameworks is used. Consequently, proofs of termination properties derived in one framework often have to be redone for others. In this talk I will study the relations between the various frameworks, and identify simple transformations which make it possible to move to a different formalism.

Matthias Raffelsieper: Productivity of Non-Orthogonal Term Rewrite Systems
Productivity is the property that finite prefixes of an infinite constructor term can be computed using a given term rewrite system. Hitherto, productivity has only been considered for orthogonal systems, where non-determinism is not allowed. In this talk, techniques are presented to also prove productivity of non-orthogonal term rewrite systems. For such systems, it is desired that one does not have to guess the reduction steps to perform, instead any outermost- fair reduction should compute an infinite constructor term in the limit.
As a main result, it is shown that for possibly non-orthogonal term rewrite systems this kind of productivity can be concluded from context-sensitive termination. This result can be applied to prove stabilization of digital circuits, as will be illustrated by means of an example.