Search

We present a novel application of hyperedge replacement grammars, showing that they can serve as an intuitive formalism for abstractly modeling dynamic data structures. The aim of our framework is to extend finite-state verification techniques to handle pointer-manipulating programs operating on complex dynamic data structures that are potentially unbounded in their size. The idea is to represent both abstraction mappings on user-defined dynamic data structures and the (abstract) semantics of pointer-manipulating operations using graph grammars, supporting a smooth integration of the two aspects. We demonstrate how our framework can be employed for analysis and verification purposes, e.g., to prove that a procedure preserves structural invariants of the heap.

We present a novel approach to the verification of concurrent pointer-manipulating programs with dynamic thread creation and memory allocation as well as destructive updates operating on arbitrary (possibly cyclic) singly-linked data structures. Correctness properties of such programs are expressed by combining a simple pointer logic for specifying heap properties with linear-time (LTL) operators for reasoning about system executions. To automatically solve the corresponding model-checking problem, which is undecidable in general, we abstract from non-interrupted sublists in the heap, resulting in a finite-state representation of the data space. We also show that the control flow of a concurrent program with unbounded thread creation can be characterized by a Petri net, making LTL model checking decidable (though not feasible in practice). In a second abstraction step we also derive a finite-state representation of the control flow, which then allows us to employ standard LTL model checking techniques.

We study the effect of an optimizing algorithm for straight-line code which first constructs a directed acyclic graph representing the given program and then generates code from it. We show that this algorithm produces optimal code with respect to the classical transformations known as Constant Folding, Common Subexpression Elimination, and Dead Code Elimination. In contrast to the former, the latter are also applicable to iterative code containing loops. We can show that the graph-based algorithm essentially corresponds to a combination of the three classical optimizations in conjunction with Copy Propagation. Thus, apart from its theoretical importance, this result is relevant for practical compiler design as it potentially allows to exploit the optimization potential of the graph-based algorithm for non-linear code as well.