The paper “Approximately Compatible Graph Predicates: Verifying Program Termination using Graph Grammars” by Alexander Ferber, Ira Fesefeldt, Thomas Noll and Emmett Rayes has received the EATCS Best Paper Award at the 19th International Conference on Graph Transformation (ICGT 2026) in Rennes, France.

It introduces a novel technique to verify termination of imperative programs supporting heap-manipulating operations and especially dynamic data structures. The idea is to use graph grammars (more exactly: hyperedge-replacement grammars) to guide abstraction of data structures, and to annotate the grammar by logical formulae that reason about quantitative properties of data structures (such as list sizes) to provide the termination argument.