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. Juggy

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.


DOIMihaela Sighireanu, Juan A. Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomas Vojnar, Constantin Enea, Ondrej Lengal, Chong Gao, Zhilin Wu. SL-COMP: Competition of Solvers for Separation Logic. TACAS 2019, Volume 11429 of LNCS, pages 116–132, Springer, 2019.
DOIHannah 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.
Show all


Show all