Automated formal methods for reliable software components

点击翻译按钮获取中文摘要

In my research program I work on software verification, which is a method that takes as input a program and gives the user feedback about possible bugs in the program. We already use such techniques today, in our compilers: they check if we use all variables and functions properly, according to their types and signatures, respectively. As a next step towards the ultimate goal of error-free programs, we develop the technology needed for checking semantical properties, e.g., if data structures on the heap are consistent, or if some forbidden variable value is possible during program execution. Theoretically, these checks are undecidable, but in practice, due to several recent breakthroughs in program verification, there is a strong hope that we can actually verify many interesting properties. The problem is identified and widely acknowledged as a grand challenge in computer science, and only an enormous effort of many research groups together can develop all the techniques that at the end make it possible to achieve the ideal of software engineering: verified software.