Formal Verification
In August 2003 I joined the Formal Methods Groups that is part of the Computer Engineering Group at the University of Tübingen.The research focus in our group lies on exploring techniques, data structures and algorithms for verification of hardware and software systems. The verification approach can be either purely formal (model checking, symbolic simulation), functional (simulation, monitoring) or a combination of these techniques. We also investigate means to describe and check properties of systems using temporal logics like PSL, LTL, and CTL, optionally augmented with time bounds on the temporal operators.
One of our main goals is to accompany theoratical work with tools that prove the feasibility of the approach. These tools are embedded into GUIs to provide an integrated verification environment for experienced verification engineers, but also for users with a less formal background. Please have a look at the tools section of our group's website.
Generic Programming
The field of research I have been working in during my time as doctoral candiadate at the Computeralgebra Group at the University of Tübingen is generic programming.By generic programming we understand employing parametric polymorphism at the programming language level. This technical approach is augmented by a thorough examination of the problem domain which results in a set of abstract concepts. Concepts constitute a collection of requirements which specify the validity of instantiations of parameterized algorithms and data structures, or more general, generic components. The concepts resulting from domain analysis are correlated and this hierarchy of concepts describes the domain's conceptual structure. Generic programming involves determining abstract concept hierarchies and implementing corresponding components, models of these concepts.
We arrive at a more abstract notion of components than usually achieved with technologies like CORBA, the COM family, or Java Beans. The set of requirements constituting a concept should on the one hand contain enough information to guarantee the correctness of instances generated from generic components. On the other hand, the requirements should be minimal in order not to restrict the possible instantiation types unnecessarily. These properties of generic components foster code re-use and interoperability, even with classical components.
Overall, generic programming leads to clearly structured libraries, collections of generic components, and applications built using these libraries exhibit a well defined system architecture.