ISBN 9783843921770

978-3-8439-2177-0, Reihe Informatik

Jonathan Heinen
Verifying Java Programs – A Graph Grammar Approach

223 Seiten, Dissertation Rheinisch-Westfälische Technische Hochschule Aachen (2015), Hardcover, B5

Zusammenfassung / Abstract

This thesis presents the framework Juggrnaut for the analysis and verification of object-oriented programs.

The core of the framework is to yield finite abstract state spaces by abstraction of heap structures via hypergraphs and hyperedge replacement grammars. For Java Bytecode it introduces a semantics defining finite abstract state spaces for Java Programs. On these state spaces classical finite state techniques such as model checking can be applied.

Properties of states are expressed by MSO, a very expressive logic that unfortunately is also hard to check. In this thesis a novel approach to check MSO on abstract states is given. To verify dynamic properties of objects during runtime classical model checking approach is extend by a tracking of state objects.

Case studies evaluate the proposed techniques with respect to their feasibility.