CPA-SEL: Collaborative Research - Continuing Progress Toward Verified Software

大多数工程制品，如桥梁和核电站，都是通过对它们进行操作条件和观察结果来进行测试的。软件是不同的。它在计算机上运行时表现出动态行为，软件质量(关于实现指定行为)通常以这种方式进行测试。但软件也可以被认为是纯粹的符号--指令的序列--因此可以接受正确性的数学证明。实现这样的“经过验证的软件”被认为是计算研究的“重大挑战”。该项目的跨学科软件工程师和逻辑学家团队的工作重点是这样一个主题：通过将仔细的语言设计与自动化定理证明的最新进展相结合，实用、可扩展、自动化的软件验证是可行的，一次一个组件。我们的计划是通过为一组基准软件组件(如计算课程和商业软件中使用的组件)生成逻辑验证条件，并自动证明它们，来对本论文进行经验性评估。该项目的意义将来自它的概念证明，验证的软件这一重大挑战是可以克服的，以及更好地理解需要向下一代软件工程师教授什么来生产验证的软件。

Most engineered artifacts, such as bridges and nuclear power plants, are tested by subjecting them to operating conditions and observing results.Software is different. It manifests dynamic behavior when running on computers, and software quality (with respect to achieving specifiedbehavior) is normally tested that way. But software also can be considered purely symbolic -- a sequence of instructions -- and hence can be subjected to mathematical proof of correctness. Achieving such "verified software" has been identified as a "grand challenge" for computing research. The work of this project's interdisciplinary team of software engineers and logicians focuses on the thesis that practical, scalable, automated software verification is feasible, one component at a time, by combining careful language design with recent advances in automated theorem proving. The plan is to evaluate this thesis empirically by generating the logical verification conditions for a benchmark suite of software components like those used in computing courses and commercial software, and proving them automatically. The project's significance will derive from its proof of concept that the verified software grand challenge can be conquered, and from a better understanding of what the next generation of software engineers need to be taught to produce verified software.