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

CPA-SEL：协作研究 - 不断取得验证软件的进展

• 批准号: 0811737
• 负责人: Bruce Weide
• 金额: $ 23.26万
• 依托单位: Ohio State University Research Foundation -DO NOT USE
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-09-01 至 2013-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0811737&HistoricalAwards=false
• 关键词: CPA; SEL; Collaborative; Research; Continuing

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.

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