SHF: Medium: Collaborative Research: Specification and Mathematics Engineering for the Verified Software End-Game

软件对现代生活非常重要。 控制几乎所有主要机器和通信系统（从飞机和汽车到医疗记录和金融交易）的软件的正确和安全行为是关键任务，往往是生死攸关的问题。 目前用于评估软件正确性的行业标准方法，称为“软件测试”，并不是万无一失的。 这个研究项目将结合联合收割机的跨学科专业知识的研究人员在软件工程和数学逻辑，以支持一个范式转移到“验证软件”：程序已经完全和机械证明，使用正式的数学逻辑，是正确的相对于完整的行为规范，他们应该做什么，他们不应该做什么。 考虑到正确的软件对社会的广泛利益及其对国家竞争力的影响，美国在经过验证的软件研究和教育方面的强大存在必须成为国家的优先事项。虽然研究思想向实践的转变需要时间，但基于对象的顺序软件验证编译器的想法非常接近现实。 在什么可以适当地描述为“游戏结束”，广泛的实证研究验证条件（VC）正确的软件已经进行。 VC是一种断言，当且仅当它们可以被证明时，程序才是正确的。 已经观察到，当VC不能被机械地证明时，障碍在于证明对数学家来说“显而易见”的VC，以及工程规范和支持数学，因此它们导致对自动证明器也“显而易见”的VC。 该项目的预期成果是在自动化软件验证中实现编程语言和工具独立的改进，这将广泛适用。 另一个关键项目目标是将支持验证软件的新概念和工具集成到本科和研究生计算机科学课程中。 这些努力将有助于发展一个优秀的下一代软件工程队伍的上级。

Software is remarkably important to modern life. The correct and secure behavior of software that controls nearly all major machines and communications systems, from aircraft and cars to medical records and financial transactions, is mission-critical and often can be a matter of life and death. The current industry-standard method for assessing correctness of software, known as "software testing", is not foolproof. This research project will combine the interdisciplinary expertise of the investigators in software engineering and mathematical logic to support a paradigm shift toward "verified software": programs that have been entirely and mechanically proved, using formal mathematical logic, to be correct relative to full behavioral specifications of what they are supposed to do and what they are not supposed to do. Given the broad benefits of correct software to society and its impact on national competitiveness, a strong U.S. presence in verified software research and education must be a national priority.While transition of research ideas to practice will take time, the idea of a verifying compiler for sequential, object-based software is tantalizingly close to reality. In what can be properly described as the "end game", extensive empirical studies of Verification Conditions (VCs) for correct software already have been undertaken. VCs are assertions that establish that a program is correct if and only if they can be proved. It has been observed that when VCs are not provable mechanically, the obstacles lie in proving VCs that are "obvious" to mathematicians, and in engineering specifications and supporting mathematics so they lead to VCs that are also "obvious" to automated provers. The expected results of this project are programming language- and tool-independent improvements in automated software verification that will be widely applicable. Another key project goal is integration of new concepts and tools supporting verified software into undergraduate and graduate Computer Science courses. These efforts will contribute to development of a superior next-generation software engineering workforce.