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.