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

软件在现代生活中非常重要。控制几乎所有主要机器和通信系统的软件的正确和安全行为，从飞机和汽车到医疗记录和金融交易，都是关键任务，往往可能是生死攸关的问题。目前被称为“软件测试”的评估软件正确性的行业标准方法并不是万无一失的。这个研究项目将结合软件工程和数理逻辑研究人员的跨学科专业知识，以支持向“验证软件”的范式转变：使用形式化数理逻辑完全和机械地证明程序相对于它们应该做什么和不应该做什么的完整行为规范是正确的。鉴于正确软件对社会的广泛益处及其对国家竞争力的影响，美国在经过验证的软件研究和教育中的强大存在必须是国家的优先事项。尽管将研究想法转化为实践需要时间，但针对顺序的、基于对象的软件的验证编译器的想法非常接近现实。在可以恰当地描述为“最终游戏”的情况下，已经对正确软件的验证条件(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.