Personal tools
You are here: Home Events Abstract Archives 2007-2008 Correct and Efficient Software Systems: Pie in the Sky or Viable Vision?

Correct and Efficient Software Systems: Pie in the Sky or Viable Vision?

Sabine Glesner Technische Universit├Ąt Berlin 4pm Tuesday 20th November 2007 Room 2511, JCMB, King's Buildings Joint ICSA/LFCS Seminar

The construction of correct software has been an important goal since the early days of computer science and has remained so ever since. An even bigger challenge is keeping the efficiency of correct systems comparable to that of non-verified ones. Since information-based systems are also being increasingly used in safety-critical areas of our lives, ensuring the reliability and correctness of such systems is an urgent problem. There is also a growing demand for improved reliability among the customers of less safety-critical systems, who only a couple of years ago were mainly concerned with enhancing efficiency and functionality.

In this talk, I demonstrate how it is possible to construct systems that are both efficient and correct. This question arises at almost all levels of system and software construction, from software component systems to compilers to hardware/software co-design. I discuss typical problems and solutions relating to the verification of optimizing compilers as well as that 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 other application areas as well. I conclude by giving an overview of further research topics being pursued in my group.

Document Actions