ISR 2015 | Program | Posters | Registration | Local Information | Lecture Notes

ISR 2015: Lectures


Basic Track

Advanced Track

The Proceedings contain extended course descriptions, including motivation, outline, prerequisites, and example problems.


The preliminary schedule for the advanced track is:

Mon Tue Wed Thu Fri
09:00-10:30 Termination Termination Termination SAT/SMT SAT/SMT
11:00-12:30 PVS PVS Program Transformation Program Transformation Program Transformation
16:00-17:30 Protocol Analysis Protocol Analysis - Graph Programming Graph Programming

The basic track runs in parallel (all slots).

Basic Track

Introductory Course

Aart Middeldorp and Sarah Winkler, Institute of Computer Science, University of Innsbruck, Austria

Term rewriting is a conceptually simple, but powerful abstract model of computation which underlies much of declarative programming and automated theorem proving. The foundation of rewriting is equational logic. It constitutes a basic framework for program analysis and has applications in automated reasoning, algebra, computability theory and lambda calculus, compiler construction, engineering, as well as functional and logic programming.

This course provides a modern introduction to rewriting in general and term rewriting in particular. All key concepts are covered and glimpses into current research will be provided. Moreover, several automatic tools will be demonstrated.

For this course, students can take an exam. Please mention on your registration whether you want this.
Aart Middeldorp is professor at the University of Innsbruck and a leading researcher in term rewriting. He has taught courses on term rewriting world-wide for more than 25 years.
Sarah Winkler is a postdoctoral researcher at the University of Innsbruck. She obtained her doctoral degree in 2013 on a topic in completion and is the main developer of the powerful completion tool mkbTT.

Advanced Track

We assume that a participant of the advanced track should be familiar with the following notions: abstract reduction systems, universal algebras, equational problems, confluence, termination and completion. All these notions are introduced in chapters 1-7 of the standard textbook "Rewriting and All That" by Franz Baader and Tobias Nipkow.

Rewriting Techniques for Correctness of Program Transformations

David Sabel and Manfred Schmidt-Schauß, Computer Science Institute, Goethe-University Frankfurt am Main, Germany

The course gives an introduction to program transformations, their correctness and rewriting techniques to reason about the correctness. The course focuses on small-step operational semantics of functional programming languages which can be seen as higher-order rewriting with a fixed strategy. On top of the operational semantics contextual equivalence is used as the main notion of program semantics and correctness of program transformations. The course also treats non-deterministic and concurrent extensions of functional programming languages and adaptions of the contextual semantics.

David Sabel received his diploma in computer science from Goethe-University Frankfurt in 2003, his Dr. in 2008 from Goethe-University Frankfurt and in 2013 his habilitation in computer science. His research focuses on programming languages semantics, and he gave several lectures on functional and concurrent programming and the semantics of programming languages. He currently holds a post-doc position at Goethe-University Frankfurt.

Manfred Schmidt-Schauß received his diploma in Mathematics from the University of Mainz in 1979 and his Dr. from the University of Kaiserslautern in 1988 in Computer Science. Since 1992 he is full professor for Artificial Intelligence and Software Technology at the Department of Computer Science of
the Goethe-University Frankfurt. Main research areas and publications are in automated deduction, unification, knowledge representation, functional programming, contextual semantics of functional programs and methods to show correctness, and algorithms on grammar-compressed compressed terms.

Algebraic Semantics of Higher-Order Abstract Syntax and Second-Order Rewriting

Makoto Hamana, Department of Computer Science, Gunma University, Japan

The algebraic semantics for term rewriting systems by monotone algebras constitutes an important foundation of TRS, refining the connection between equational logic and universal algebra. It has also fruitful applications, such as the interpretation method to prove termination of TRS. What about higher-order rewriting?

In this course, we move one step further to study the algebraic semantics for second-order rewriting systems, particular Klop's combinatory reduction systems (CRS). We uniformly generalise syntax and algebras to the second-order setting, i.e. higher-order abstract syntax and second-order algebras. Then we elucidate that, as in the case of TRS, tight connections exist among second-order equational logic, second-order algebra and CRS.

Therefore, this course includes introduction to CRSs, higher-order abstract syntax, their algebraic semantics, and their application to termination problems of CRS.

Makoto Hamana is an assistant professor at Computer Science Department, Gunma University, Japan. He have spent his Ph.D study at Prof. Ida and Dr. Middeldorp's group at University of Tsukuba and obtained Ph.D there in 1998. After that, he became a JSPS (Japan Society of Promotion of Science) research fellow and stayed at LFCS, University of Edinburgh by invitation by Prof. Gordon Plotkin and Dr. John Power.

Term Rewriting applied to Cryptographic Protocol Analysis: the Maude-NPA tool

Santiago Escobar, DSIC-ELP, Universitat Politècnica de València, Spain

In this course we give an overview of the theoretical and practical aspects of the Maude-NRL Protocol Analyzer (Maude-NPA). Maude-NPA is a tool for the symbolic analysis of cryptographic protocols. It searches backwards from a pattern defining secrecy and/or authentication properties of a protocol and it is able to find an attack or prove the absence of any attack. Maude-NPA is designed to take account of the algebraic properties of the crypto systems involved (e.g., exclusive-or, Diffie-Hellman, etc.) in order to give a more complete representation of both the protocol and the attackers capabilities. During the development of the tool we have also defined new theoretical and practical frameworks such as variant-based unification, logical model checking, asymmetric unification, or state-space optimizations that will be presented during the course.

Santiago Escobar is associate professor at the Universitat Politècnica de València (UPV), Spain. His research interests include formal methods, security, verification, model checking, rewriting, narrowing, and evaluation strategies. His works on narrowing have been discovered to be essential for narrowing-based applications such as equational unification, model checking, or protocol analysis. In the security area, he has developed the Maude-NPA cryptographic protocol analyzer in collaboration with Catherine Meadows from the Naval Research Laboratory of Washington D.C. and Jose Meseguer from the University of Illinois at Urbana-Champaign. This is the state-of-the-art tool for verification of protocols with advanced cryptographic properties. Dr. Escobar received a M.Sc. in 1998 and a Ph.D. in Computer Science in 2003 at the Universitat Politècnica de València.

SAT/SMT encodings for rewrite problems

Hans Zantema, Department of Computer Science, TU Eindhoven, The Netherlands

For automatically checking whether a rewrite system satisfies some property, applying SAT solving has shown up to be extremely useful. The presentation will be split up into the following parts. In the first part it is shown how various constraint problems independent from rewriting can be expressed and solved by SAT/SMT solving, and some basic theory is presented. Next there is a practical slot in which students solve exercise problems, using SAT/SMT tools on their laptop. In the last part it will be shown how this approach can be applied for rewriting problems, in particular, proving termination and non-termination of rewriting.

Hans Zantema is associate professor at Eindhoven University of Technology and part time full professor at Radboud University in Nijmegen. He did his PhD in algebraic number theory in 1983. Since 1990 one of his main research interests is in rewriting; first with a focus on termination, later on with a focus on both applying SAT solving and on infinite data structures.

Higher-Order Rewriting

Femke van Raamsdonk, VU University, Amsterdam, The Netherlands

Higher-order rewrite rules may contain bound variables and variables ranging over functions. Higher-order rewriting extends the λ-calculus by allowing the presence of function symbols and rewrite rules describing their operational semantics. It extends first-order rewriting by the presence of binders. So when proving properties in higher-order rewriting, one has to deal with both substitution as in the λ-calculus, and with algebraic combinatorics as in term rewriting.

This course provides an introduction to higher-order rewriting. We discuss the setting of higher-order rewriting, examples of higher-order rewrite systems, results concerning confluence and termination, and counterexamples to some proof methods.

Femke van Raamsdonk completed her PhD on higher-order rewriting in 1996. Her research interests are rewriting and lambda-calculus, models of computation, type theory and verification. Femke has taught several courses in the bachelor and master curricula of computer science, and in summer schools. She is an assistant professor in the theoretical computer science group at the VU University in Amsterdam, The Netherlands.

Proving Abstract Rewriting Properties with PVS

Alfons Geser, HTWK Leipzig, Germany

This course teaches the use of the PVS theorem prover to prove basic theorems in abstract rewriting, such as the Church/Rosser theorem, Newman's Lemma, or the characterization of conversion by rewriting to normal form. PVS judgements are used to simplify proving.

Alfons Geser received his diploma in Computer Science at the Technical University of Munich in 1984, his Dr. at the University of Passau in 1991, and his habilitation at the University of Tübingen in 2002. Since 2005 he is a full professor for Applied Computer Science at the Faculty of Electrical Engineering and Information Technology at the HTWK Leipzig. Research areas with publications are Termination of Rewriting, Parallelization, Theorem Proving, Formal Verification, and Fault Tolerant Protocols. Dr. Geser is a contributor to the NASA Langley PVS library.

Termination and Complexity

Georg Moser, Institute of Computer Science, University of Innsbruck, Austria

A fundamental property of rewrite systems is termination, the non-existence of endless rewrite steps. Conclusively strong techniques have been designed to ensure termination of term rewrite systems. Already some time ago, the emphasis shifted towards techniques that automatically verify termination of a given term rewrite system. The annual termination competition showcases the remarkable success rate that can nowadays be obtained by fully automated termination tools. This naturally entails investigations into the complexity of term rewrite systems. A term rewrite system is considered of higher complexity, if the number of possible rewrite steps is larger.

The course provides an advanced understanding in the topics of termination and complexity of term rewrite systems. For both topics automated techniques are presented.

Georg Moser received his PhD in Computer Science and his MSc in Computational Logic from the Vienna University of Technology. In addition he holds a MSc from the University of Leeds. In 2009, he received his habilitation in Computer Science from the University of Innsbruck. Since 2011, he is an associate professor at the Institute of Computer Science of the University of Innsbruck, Austria. Furthermore he heads the research group Computation with Bounded Resources. His main research is concerned with program analysis, term rewriting, logic, and proof theory. His achievements in this area fall into two main areas: structural proof theory and complexity analysis.

Rule-based Graph Programming

Detlef Plump, The University of York, United Kingdom

This short course introduces GP 2, a rule-based domain-specific language for graphs. The language is non-deterministic and computationally complete, and has a simple syntax and semantics to facilitate formal reasoning. A number of example programs and their properties will be discussed, and their execution with the GP 2 implementation demonstrated. The course will also explain the graph transformation framework underlying GP 2, the so-called double-pushout approach with relabelling. Based on this approach, a formal semantics of GP 2 in the style of structural operational semantics will be presented. Current research such as formal program verification with a Hoare-style proof calculus will be briefly addressed, too.

Detlef Plump is a senior lecturer (associate professor) in the Department of Computer Science at the University of York. He received his doctorate in 1993 from the University of Bremen for his thesis "Evaluation of Functional Expressions by Hypergraph Rewriting". In 1999, he obtained habilitation in computer science from the University of Bremen. He has been a member of the Steering Committee of the International Conference on Graph Transformation since 2002 and a member of the Steering Committee of the International Workshop on Computing with Terms and Graphs since September 2005. At York, he regularly teaches the course "Computing by Graph Transformation" to undergraduate students.

ISR 2015, August 10-14, F-IMN, HTWK Leipzig, Germany. | Legal Note (Impressum)