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.

Publications

2019
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.
2018
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.
2017
DOIChristina Jansen. Static Analysis of Pointer Programs – Linking Graph Grammars and Separation Logic. Phd Thesis at RWTH Aachen University, 2017.
LinkHannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness. Technical report at arxiv number 1705.03754, 2017.
DOIChristina 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.
LinkMarieke Huisman, Thomas Noll, Makoto Tatsuta. Analysis and Verification of Pointer Programs. Technical report at National Institute of Informatics number 2017-14, 2017.
2016
LinkChristina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Technical report at arXiv number 1610.07041, 2016.
2015
DOIJonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Juggrnaut: Using Graph Grammars for Abstracting Unbounded Heap Structures. Formal Methods in System Design 47(2), pages 159–203, 2015.
LinkChristoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic. Technical report at RWTH Aachen University number AIB-2015-12, 2015.
LinkChristina Jansen. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs. Proceedings of the Young Researchers’ Conference “Frontiers of Formal Methods”, Volume of Aachener Informatik Berichte, pages 145-150, RWTH Aachen, 2015.
DOIJonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying Pointer Programs using Graph Grammars. Science of Computer Programming 97, pages 157–162, 2015.
DOIChristoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic. Programming Languages and Systems (APLAS 2015), Volume 9458 of LNCS, pages 90–108, Springer, 2015.
2014
LinkChristina Jansen, Florian Göbe, Thomas Noll. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs. Technical report at RWTH Aachen University number AIB-2014-08, 2014.
DOIChristina Jansen, Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs. Proc. 7th Int. Conf. on Graph Transformation (ICGT 2014), Volume 8571 of LNCS, pages 49–64, Springer, 2014.
DOIChristina Jansen, Florian Göbe, Thomas Noll. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs. Proc. 7th Int. Conf. on Graph Transformation (ICGT 2014), Volume 8571 of LNCS, pages 65–80, Springer, 2014.
2013
LinkMarkus Bals, Christina Jansen, Thomas Noll. Incremental Construction of Greibach Normal Form for Context-Free Grammars. Proc. Int. Symp. on Theoretical Aspects of Software Engineering (TASE 2013), pages 165–168, IEEE Computer Society, 2013.
2012
DownloadLinkJonathan Heinen, Christina Jansen, Henrik Barthels. Juggrnaut - An Abstract JVM. 2nd Int. Conf. on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Volume 7421 of LNCS, pages 142–159, Springer, 2012.
2011
DownloadLinkJonathan Heinen, Christina Jansen. Juggrnaut - An Abstract JVM. Formal Verification of Object-Oriented Software. Papers presented at the 2nd International Conference, October 5-7, 2011, Turin, Italy, Volume 2011 of Karlsruhe Reports in Informatics, pages 226–243, Karlsruhe, 2011.
DownloadLinkJonathan Heinen, Christina Jansen. Juggrnaut - An Abstract JVM. Technical report at RWTH Aachen University, Germany number AIB 2011-21, 2011.
DownloadLinkChristina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars. 5th Int. Conf. on Language and Automata Theory and Applications (LATA 2011), Volume 6638 of LNCS, pages 323–335, Springer-Verlag, 2011.
DownloadLinkChristina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars. Technical report at RWTH Aachen University, Germany number AIB 2011-04, 2011.
2010
DOILinkJonathan Heinen, Thomas Noll, Stefan Rieger. Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures. Proc. 3rd Int. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2009), Volume 266 of ENTCS, pages 93–107, Elsevier, 2010.
2009
Stefan Rieger. Verification of Pointer Programs. Phd Thesis at RWTH Aachen University, 2009.
2008
LinkLinkStefan Rieger, Thomas Noll. Abstracting Complex Data Structures by Hyperedge Replacement. 4th Int. Conference on Graph Transformations (ICGT 2008), Volume 5214 of LNCS, pages 69–83, Springer, 2008.

Talks