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