Verifying Java Programs – A Graph Grammar Approach

Beschreibung

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.

Autor*in

Jonathan Heinen

Themen in »Verifying Java Programs – A Graph Grammar Approach«

Graph Grammar Approach Java Java Programs

Stimmen zu »Verifying Java Programs – A Graph Grammar Approach«

Details

Link teilen