We present a graph-based tool for analysing Java programs operating on dynamic data structures. It involves the generation of an abstract state space employing a user-defined graph grammar. LTL model checking is then applied to this state space, supporting both structural and functional correctness properties. The analysis is fully automated, procedure-modular, and provides informative visual feedback including counterexamples in the case of property violations. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

This paper presents an incremental version of the well-known algorithm for constructing the Greibach normal form (GNF) of a context-free string grammar. It supports the extension of the grammar by additional rules without the need of reperforming the GNF construction from scratch. Thus it offers an efficiency advantage over the classical GNF algorithm in use cases where grammars are extended at a later stage. It ensures that nonterminals and production rules once generated during GNF construction are not removed due to recomputation of GNF, thus preserving the structure of derivations. We present a commandline tool implementing both the classical and the incremental GNF algorithm and compare both by means of two case studies.