|
      
|
|
|
|
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.
