ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 11:30 - 12:00 at SUN II - Program Analysis and Automated Verification Chair(s): Stephanie Balzer

We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework.

The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.

Thu 11 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
Program Analysis and Automated VerificationESOP at SUN II
Chair(s): Stephanie Balzer Carnegie Mellon University
10:30
30m
Talk
Data-Races and Static Analysis for Interrupt-Driven Kernels
ESOP
Link to publication
11:00
30m
Talk
An abstract domain for trees with numeric relations
ESOP
Matthieu Journault , Antoine Miné UPMC, France, Abdelraouf Ouadjaout Sorbonne Université
Link to publication
11:30
30m
Talk
A static higher-order dependency pair framework
ESOP
Carsten Fuhs Birkbeck, University of London, Cynthia Kop Radboud University Nijmegen
Link to publication
12:00
30m
Talk
Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
ESOP
Henning Basold CNRS & ENS Lyon, Ekaterina Komendantskaya Heriot-Watt University, UK, Yue Li Heriot-Watt University, UK
Link to publication