The construction of correct software has been an important goal since the commencements of computer science and has not lost importance ever since. It is an even bigger challenge to keep the efficiency of correct systems comparable to that of non-verified ones. Since information-based systems are used increasingly also in safety-critical parts of our lives, it is an urgent problem how reliability and correctness of such systems can be ensured. Also customers of less safety-critical systems more and more demand to improve reliability whereas a couple of years ago, enhancing efficiency and functionality has been their primary interest.
In this talk, I demonstrate how efficient as well as correct systems can be constructed. This question comes up on almost all levels of system and software construction, starting from software component systems, to compilers, to hardware/software co-design. I discuss typical problems and solutions from the area of verification of optimizing compilers as well as from the area of verification of model transformations and model-driven software development. I not only show how correctness proofs formulated in theorem provers can be connected to real software systems but also demonstrate how the proof principles employed during verification can be reused in further application areas as well. Concludingly, I give an overview over further research topics in my group.
About Sabine Glesner
Sabine Glesner is Professor for Computer Science at the Technical University of Berlin. She graduated with a Master of Science in Computer Science from the University of California, Berkeley, in 1994, meanwhile being funded by a Fulbright grant. She then finished her studies in computer science at the Technical University of Darmstadt "with distinction", thus receiving an Informatik-Diplom in 1996. In 1999, Sabine Glesner obtained her PhD in computer science "with distinction" at the University of Karlsruhe and shared the Förderpreis des Forschungszentrums Informatik for the best PhD thesis in the computer science department in Karlsruhe in 1999. In 2005, she finished her habilitation. In the same year, she accepted an offer of a professorship from the Technical University of Berlin and rejected another one at the University of Rostock. Her research has been funded, among others, by the Aktionsplan Informatik as part of the Emmy Noether-Programm of the German Science Foundation (DFG). Sabine Glesner works as referee and program committee member for international conferences and journals and is editor-in-chief of the journal Computer Science – Research and Development (previously known as Informatik – Forschung und Entwicklung). Her current research focuses on software engineering for embedded systems, with special emphasis on verification and validation, optimizing compilers and hardware/software co-design.