Juggrnaut: Verifying Pointer Programs with Unbounded Heap Structures
Juggrnaut (Just Use Graph GRammars for Nicely Abstracting Unbounded sTructures) is an abstraction framework for Java Bytecode which allows to automatically derive abstract versions of pointer-manipulating operations.
States of the JVM are modeled as hypergraphs, and both pointer operations and abstraction mappings are represented by hypergraph transformations. More concretely we employ hyperedge replacement grammars to specify data structures and their abstractions. The key idea is to use the replacement operations which are induced by the grammar rules in two directions. By the backward application of some rule, a subgraph of the heap can be condensed into a single nonterminal edge, thus obtaining an abstraction of the heap. By applying rules in forward direction, certain parts of the heap which have been abstracted before can be concretized again.
|Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs. Proc. CAV 2018, Part II, Volume 10982 of LNCS, pages 3–11, Springer, 2018.|
|Christina Jansen. Static Analysis of Pointer Programs – Linking Graph Grammars and Separation Logic. Phd Thesis at RWTH Aachen University, 2017.|
|Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness. Technical report at arxiv number 1705.03754, 2017.|
|Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Proc. ESOP 2017, Volume 10201 of LNCS, pages 611–638, Springer, 2017.|
|Marieke Huisman, Thomas Noll, Makoto Tatsuta. Analysis and Verification of Pointer Programs. Technical report at National Institute of Informatics number 2017-14, 2017.|