From July 25 to 28, our group hosts the Summer meeting of the AADL Standardization Committee. The Architecture Analysis and Design Language (AADL) is a modeling language for the specification, analysis, automated integration and code generation of safety-critical systems. Amongst others, it is being used in our COMPASS project for designing on-board computer-based aerospace systems.

Sebastian Junges will receive the price for the best Master Thesis in Computer Science 2014/15 in Germany. His work, entitled Simplifying Fault Trees by Graph Rewriting, has been selected by the Fakultätentag Informatik. Sebastian will be awarded the price during the 45th Annual Meeting of the German Informatics Society (Gesellschaft für Informatik e.V. – GI).

The paper entitled Juggrnaut: Using Graph Grammars for Abstracting Unbounded Heap Structures by Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen and Thomas Noll has been accepted for publication by the Formal Methods in System Design journal.  This paper presents a novel abstraction framework for heap data structures that employs graph grammars for modelling dynamic data structures, and […]

The paper entitled Tree-Like Grammars and Separation Logic by Christoph Matheja, Christina Jansen and Thomas Noll has been accepted at the 13th Asian Symposium on Programming Languages and Systems (APLAS 2015).  This paper investigates the relationship between certain classes of tree grammars and logical formalisms, especially with regard to the corresponding inclusion and entailment problems.

The paper entitled IC3 Software Model Checking on Control Flow Automata by Tim Lange, Martin Neuhäußer (Siemens AG) and Thomas Noll has been accepted at the 15th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2015).  This paper presents a method to exploit a program’s control flow for efficiently model checking its correctness properties.

The paper “Compositional Analysis Using Component-Oriented Interpolation” by Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, and Thomas Noll has received the Best Paper Award at the 11th International Symposium on  Formal Aspects of Component Software (FACS 2014). It presents a novel abstraction technique that exploits the compositionality of a concurrent system consisting of interacting components.

The papers “Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs” by Christina Jansen, Florian Göbe, and Thomas Noll, and “Generating Abstract Graph-Based Procedure Summaries for Pointer Programs” by Christina Jansen and Thomas Noll have been accepted at ICGT 2014 in York, GB.  The former paper relates two abstraction approaches for pointer programs, graph grammars and […]