Sep 14, 2010: Eduardo Zambon: Neighbourhood Abstraction in GROOVE

September 14, 2010Neighbourhood Abstraction in GROOVE
Room: Zi 5126Eduardo Zambon

In this talk I will discuss my ongoing work on abstraction of graph transformation systems. Important classes of such systems have unbounded state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. The talk is divided in two parts. In the first part I will give an overview of the theory of neighbourhood abstraction. The second part will cover key points of the implementation of this theory in GROOVE. To appear in the GraBaTs'10 workshop.