EATCS Best Paper Award

König, Barbara (Recipient), Rensink, Arend (Recipient), Stoltenow, Lara (Recipient) & Urrigshardt, Fabian (Recipient)

Prize

Description

handed out at ICGT 2025, the 18th International Conference on Graph Transformation

Awarded date	12 Jun 2025
Degree of recognition	International
Granting Organisations	European Association for Theoretical Computer Science (EATCS)

Awarded at event

Event title	18th International Conference on Graph Transformation, ICGT 2025
Location	Koblenz, GermanyShow on map
Period	11 Jun 2025 → 12 Jun 2025

Documents & Links

EATCS Best paper award, June 2025
File: application/pdf, 231 KB
Type: Text

This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.

Related content

Research output
Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review