This page gives an overview over the research conducted in our group. For each topic you will find a brief description together with the involved persons, the implemented systems and the relevant projects. If you are interested in further information, please feel free to contact any of the listed persons.
We provide fundamental constructions and algorithms for very precise program analyses. We are interested in general fast fixpoint methods. We also investigate precise methods for deriving complex program properties. E.g., we consider interval analysis or polynomial relationships between integer variables for imperative programs. We also deal with extensions of these analyses to programs with procedures.
In order to prove the absence of certain attacks to cryptographic protocols, we rely on a formalization of the relevant information by means of first-order predicate logic, perhaps enriched by equational theories describing the semantic properties of specific occurring operators. Theories of interest in this area are, e.g., ACU or the group axioms for a dedicated symbol +. In order to arrive at practical algorithms, we are particularly interested in decidable fragments of first-order logic.
XML documents are linear representations of tree-like structures. Types of XML documents are typically specified by some class of recognizable tree-language. Fundamental problems such as checking whether a given document belongs to a type or querying a given document for subdocuments with specific properties, are thus amenable to automata-techniques. In the DFG project DocML, we therefore provide a prototypical implementation of an efficient querying as well as transformation tool for XML documents. In the follow-up project we then provide automata-based methods for deciding whether a given XML transformation transforms all documents of a given input type into documents conforming to a given output type.
Within the project ULI, we have implemented the TeleTeachingTool (TTT). This tool provides flexible desktop recording as well as the possibility of realtime broacast of lectures. Due to its little technical overhead, it allows for transparent teleteaching: meaning that the teacher may fully concentrate on his lecture and the content to be transported.
Beyond the basic tool, meanwhile a wealth of additional components have emerged such as automatic index generation, a postprocessing tool, a converter into flash format etc.