Juggrnaut

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

GNF/IGNF Generator:

Command-line tool for generating (incremental) Greibach Normal Form for context-free string grammars (Diploma thesis, M. Bals).

Reading and Analysing Grammar Files:

Syntactic and Semantic Analysis of Hyperedge Replacement Grammars for Heap Abstraction (bachelor thesis).

2018
	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.
2017
	Thomas Noll. Graph-Based Abstract Interpretation of Pointer Programs, Talk at NII Shonan Seminar on Analysis and Verification of Pointer Programs, Hayama, Japan, 2017.
	Christina Jansen. The Attestor Tool - Graph-based Abstract Interpretation in Practice, Talk at NII Meeting, Shonan, Japan, 2017.
	Christina Jansen. Static Analysis of Pointer Programs – Linking Graph Grammars and Separation Logic. Phd Thesis at RWTH Aachen University, 2017.
	Christina Jansen. Graph-based Abstract Interpretation for Pointer Programs, Talk at Twente, Netherlands, 2017.
	Thomas Noll. Graph-Based Static Analysis of Concurrent Pointer Programs, Talk at WIAI-Fakultätskolloquium, Universität Bamberg, Germany, 2017.
	Daniel Cloerkes. A Cyclic Proof System for Graph Grammar Inclusion. Bachelor 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. Graph-based Abstract Interpretation for Pointer Programs, Talk at Söllerhaus, Hirschegg, 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.
2016
	Christina 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
	Thomas Noll. Modular Analysis of Concurrent Pointer Programs Using Graph Grammars, Talk at Dagstuhl Seminar on Verification of Evolving Graph Structures, Wadern, Germany, 2015.
	Jonathan 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.
	Christoph Matheja. Tree-like Grammars and Separation Logic, Talk at KPS 2015, Pörtschach, Austria, 2015.
	Christoph Welzel. Thread-Modular Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2015.
	Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic. Technical report at RWTH Aachen University number AIB-2015-12, 2015.
	Christina 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.
	Christina Jansen. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs, Talk at FFM 2015, 2015.
	Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying Pointer Programs using Graph Grammars. Science of Computer Programming 97, pages 157–162, 2015.
	Christoph 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
	Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs, MOVES Seminar Talk at RWTH Aachen University, Germany, 2014.
	Christoph Matheja. Reconciling Decidability of Separation Logic Entailment and Graph Grammar Language Inclusion. Master Thesis at RWTH Aachen University, 2014.
	Christina Jansen. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs, Talk at 7th Int. Conference on Graph Transformation (ICGT 2014), 2014.
	Christina 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.
	Christina 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.
	Christina 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
	Yannis Samiro Discher. Graph-Based Interprocedural Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2013.
	Christina Jansen. A Graph-Based Approach to Heap Abstraction, Seminar Talk at AlgoSyn Seminar, 2013.
	Christina Jansen. Juggrnaut - A Graph-Based Approach to Heap Abstraction, Talk at Queen Mary University London, 2013.
	Markus 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
	Florian Göbe. Transformation von Separation Logic Prädikaten durch Hyperkantenersetzungsgrammatiken. at RWTH Aachen, 2012.
	Max Görtz. Deciding MSO over Languages of Hypergraphs. Bachelorthesis at RWTH Aachen University, 2012.
	Alexander Dominik Weinert. Inferring Heap Abstraction Grammars. Bachelor Thesis at RWTH Aachen University, 2012.
	Tobias Hoffmann. Model Checking Quantifizierter Linearer Temporaler Logik über Pointerprogrammen. Diplomarbeit at RWTH Aachen University, 2012.
	Jonathan Heinen. Analysis and Verification of Heap-Manipulating Programs, Talk at D-CON 2012, Kaiserslautern, 2012.
	Christina Jansen. Verifying Pointer Programs Using Hyperedge Replacement Grammars, Talk at ULB Bruxelles, 2012.
	Jonathan Heinen. Juggrnaut: The Analysis of Object Oriented Programs, Talk at mac, Uni Bamberg, 2012.
	Jonathan 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
	Jonathan Heinen. Juggrnaut - An Abstract JVM, Talk at the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011) Turin, Italy, 2011.
	Jonathan 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.
	Jonathan Heinen, Christina Jansen. Juggrnaut - An Abstract JVM. Technical report at RWTH Aachen University, Germany number AIB 2011-21, 2011.
	Henrik Barthels. Automata-Based Detection of Hypergraph Embeddings. Bachelorarbeit at RWTH Aachen University , 2011.
	Christina Jansen. Heap Abstraction by means of Hyperedge Replacement Grammars, Talk at YR-CONCUR 2011, 2011.
	Gereon Kremer. Syntaktische und semantische Analyse von Hyperkantenersetzungsgrammatiken zur Heapabstraktion. Bachelors Thesis at RWTH Aachen University, 2011.
	Christina Jansen. Heap Abstraction by means of Hyperedge Replacement Grammars, Talk at Summer School Marktoberdorf 2011, 2011.
	Markus Bals. Incremental Greibach Normal Form. Diploma Thesis at RWTH Aachen University, 2011.
	Christina 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.
	Christina Jansen. A Local Greibach Normal Form for Hyperedge Replacement Grammars, Talk at LATA 2011, 2011.
	Jonathan Heinen. Verification of Object Oriented Programs, Talk at Universität Duisburg-Essen, 2011.
	Jonathan Heinen. Verificación de Programas Orientados a Objetos, Talk at Universidad Nacional de Colombia, 2011.
	Jonathan Heinen. Verifying Pointer Programs Using Graph Grammars (Theory and Practice), Talk at D-CON 2011, Münster, 2011.
	Christina 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
	Joost-Pieter Katoen. Verifying Pointer Programs Using Graph Grammars, Talk at LIAFA Workshop on Automata and Logic for Data Manipulating Programs, 2010.
	Johanna Nellen. Konfluenzanalyse und Vervollständigung von Graphersetzungssystemen. Diplomarbeit at RWTH Aachen University, 2010.
	Christina Jansen. Entwicklung eines Inferenzalgorithmus für Hyperkantenersetzungsgrammatiken. Diplomarbeit at RWTH Aachen University, 2010.
	Jonathan 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.
	Christina Jansen. Generierung von Hyperkantenersetzungsgrammatiken zur Heapabstraktion, Talk at KPS 2009, 2009.
	Ralf Grossmann. Heapabstraktion durch partielle Graphreduktion mittels Graphgrammatiken . Diplomarbeit at Faculty of Mathematics, Computer Sciences and Natural Sciences,RWTH Aachen University , 2009.
	Jonathan Heinen. Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures, Talk at TTSS 2009, 2009.
2008
	Stefan 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.
2007
	Jonathan Heinen. Graph Grammar Abstraction for Complex Dynamic Data Structures, Talk at KPS 2007, Timmendorfer Strand, 2007.

BSc/MSc/Diploma Topics
Teaching WS 2012/13
Hybrid Systems Group

We are looking for a HiWi for the Compiler Construction course. If you are interested, please contact Thomas Noll.

Joost-Pieter Katoen has been appointed as a member of the renowned Academia Europaea (Academy of Europe), a European, non-governmental association acting as an Academy whose members are scientists and scholars who collectively aim to promote learning, education and research.

Vacancies for postdoctoral researchers in "Automated Analysis of Probabilistic Programs". Application deadline: August 15, 2013.

Joost-Pieter Katoen has been awarded a Distinguished Professorship from the RWTH Aachen University.

The Hybrid Systems: Computation and Control (HSCC'13) conference in Philadelphia has been very successful: Hongfei Fu received the best student paper award for his paper "Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata". Besides, the paper by Ilya Tkachev, Alexandru Mereacre, Alessandro Abate and Joost-Pieter Katoen was ranked second in the overall best paper award selection.

Joost-Pieter Katoen has been elected as Steering Committee Chair of ETAPS (www.etaps.org), the largest conference on theory and practice of software in Europe. He is the first non-UK ETAPS SC chair since the conference was initiated in 1998. More information here.

The Alumni-Magazine of RWTH Aachen University contains an interview with our former PhD student and postdoctoral researcher, Dr. Tingting Han.

HiWi's wanted to work in a new European Space Agency project for enhancing state-of-the-art design and analysis tools (COMPASS) for the next generation European rockets. Need programming and model checking affinity. See here for details and contact.

We offer openings for several PhD candidates in the area of
"Model-Based Design and Analysis for Dependable Software Systems". Deadline for application: September 14, 2012. For further information click here.

The Theory of Hybrid Systems Group offers two jobs as student assistants within the CEBug project. For more information, look here.

Dino Distefano received the prestigious Roger Needham Award for his work on software verification. This award is for a distinguished research contribution in computer science by a UK based researcher who has completed up to 10 years of post-doctoral research. Dr. Distefano was the first PhD student supervised by Joost-Pieter Katoen.

Marijn Jongerden received the German MMB (Messung, Modellierung und Bewertung von Rechensystemen) Award 2012 of the GI/ITG-Committee for Measurement, Modelling and Evaluation of Computing Systems for his PhD-thesis on "Model-based energy analysis of battery powered systems". His work was supervised by Boudewijn Haverkort (Twente) and Joost-Pieter Katoen.

Our paper "Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite" has been accepted to ICSE 2012 in the track SE in Practice (18% acceptance rate). The paper treats a new satellite from the European Space Agency that was modeled and analyzed with modern tools during the actual satellite design.

Joost-Pieter Katoen will act as DJ in the "Nacht der Professoren" in the Apollo bar and cinema.