Datenbestand vom 20. Januar 2019
Tel: 089 / 66060798
Mo - Fr, 9 - 12 Uhr
Fax: 089 / 66060799
aktualisiert am 20. Januar 2019
978-3-8439-2177-0, Reihe Informatik
Verifying Java Programs – A Graph Grammar Approach
223 Seiten, Dissertation Rheinisch-Westfälische Technische Hochschule Aachen (2015), Hardcover, B5
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.