Sep 16, 2014: Jonathan Heinen: Verifying Java Programs - A Graph Grammar Approach

September 16, 2014Verifying Java Programs - A Graph Grammar Approach
Room: Zi 2126Jonathan Heinen

Verifying object-oriented programs we encounter some additional challenges as objects can be created, manipulated and newly linked at runtime. The dynamic creation of objects imposes (potentially) infinite state spaces preventing us from using standard verification techniques.
I present a verification framework based on the abstraction of heap structures via hypergraphs and hyperedge replacement grammars which allows us to generate finite abstract state spaces. Beside the generation of the state spaces we consider the description of heap properties via MSO-formulae as well as an enhanced model checking algorithm that takes objects on the heap in consideration. Some experimental results generated with our prototype tool Juggrnaut give a hint to the abilities of our approach.