The aim of our research is to make software-based systems more trustworthy (i.e. correct, safe, and secure) than they are today. As software engineering is a complex and error-prone task, we employ formal methods for reasoning about information systems and critical system properties. We investigate software systems on the level of code (source code and machine code) as well as on the level of more abstract system specifications. This allows us to provide support for different stages of software development. More details can be found in the Research and Projects sections.
Parts of our research are funded by the Deutsche Forschungsgemeinschaft (DFG), by the European Union (EU), and, within the "Landes-Offensive zur Entwicklung Wissenschaftlich-ökonomischer Exzellenz (LOEWE)", by the Land Hessen.
In summer term 2014 we offer the following courses:
Sylvia Grewe et al. published three entries in the Isabelle Archive of Formal Proofs: A Formalization of Assumptions and Guarantees for Compositional Noninterference, A Formalization of Strong Security, and A Formalization of Declassification with WHAT-and-WHERE-Security.