Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs

Abstract

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.