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.