Automated Software Verification: Foundations and Applications

现代软件系统是令人难以置信的复杂工程工件。它们依赖于复杂的算法，由大型的，通常是分布式的团队开发，并由许多相互连接的组件构建而成。软件系统是非常难以得到正确的，验证和认证。即使在医疗设备、汽车和航空电子等安全关键行业，软件漏洞也很常见。然而，我们的社会越来越依赖于这些系统的可靠运行。安全关键系统和非安全关键系统之间的界限正在被侵蚀。

Modern software systems are incredibly complex engineered artifacts. They rely on intricate algorithms, developed by large, often distributed, teams, and are build out of many interconnected components. Software systems are extremely difficult to get right, to verify, and to certify. Software bugs are common even in such safety-critical industries as medical devices, automotive, and avionics. Yet, our society is increasingly becoming dependent on reliable operation of such systems. The border between safety- and non-safety-critical system is being eroded.