Cooperative Reasoning for Automatic Software Verification

自动软件验证的协作推理

• 批准号: EP/F037597/1
• 负责人: Andrew Ireland
• 金额: $ 38.85万
• 依托单位: Heriot-Watt University
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2008
• 资助国家: 英国
• 起止时间: 2008 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FF037597%2F1
• 关键词: Cooperative; Reasoning; Automatic; Software; Verification

The proliferation of software across all aspects of modern life means that software failures can have significant economic, as well as social impact. The goal of being able to develop software that can be formally verified as correct with respect to its intended behaviour is therefore highly desirable. The foundations of such formal verification have a long anddistinguished history, dating back over fifty years. What hasremained more elusive are scalable verification tools that can deal with the complexities of software systems.However, times are changing, as reflected by a current renaissance within the formal software verification community -- both in industryas well as academia. A significant recent development has been Separation Logic, a logic which promotes scalable reasoning forpointer programs. Pointers are a powerful and widely usedprogramming mechanism, but developing and maintaining correctpointer programs is notoriously hard. In terms of verification tools, the majority of effort has gone into developing light-weight analysis techniques for separation logic, such as shape analysis. Shape analysis ignores the contentof data, focusing instead on how data is structured. While such light-weight properties can be extremely valuable to industry,ultimately a more comprehensive level of specification is calledfor, i.e. correctness specifications. For instance, the verificationof software libraries against agreed correctness standards couldprove highly valuable across a wide range of sectors. However,to verify such comprehensive specifications requires more heavy-weight analysis, i.e. theorem proving. Our proposal focuses on the development of tools which willsupport the automatic verification of correctness specificationswithin separation logic. In particular, we will investigate how light- and heavy-weight approaches can be optimally combined. We propose a cooperative approach, in which individual techniques combine their strengths, but crucially compensate for each other's weaknesses through the communication of partial results and failures. To achieve this level of cooperation we will use a theorem proving technique called proof planning, which has a proven track-record in building cooperative reasoning tools. We plan to combine the proof planning approach with existing off-the-shelf shape analysis tools developed by Peter O'Hearn's research group at Queen Mary University (London). Note that our cooperative approach will also enhance the existing shape analysis tools, i.e. make the tools extensible and thus more widely applicable. If our cooperative style of integration is successful, then it could have a significant impact on reducing the cost of developing highly reliable software.

软件在现代生活各个方面的扩散意味着软件故障会产生重大的经济和社会影响。因此，能够开发能够被正式验证为其预期行为正确的软件的目标是非常可取的。这种正式核查的基础有着悠久而杰出的历史，可以追溯到五十多年前。更难以捉摸的是可扩展的验证工具，它可以处理软件系统的复杂性。然而，时代在变化，正如当前正式软件验证社区的复兴所反映的那样——无论是在工业界还是学术界。最近一个重要的发展是分离逻辑，这种逻辑促进了指针程序的可伸缩推理。指针是一种强大而广泛使用的编程机制，但是开发和维护正确的指针程序是出了名的困难。在验证工具方面，大部分的工作已经投入到开发用于分离逻辑的轻量级分析技术，例如形状分析。形状分析忽略数据的内容，而是关注数据的结构。虽然这种轻量级属性对工业来说非常有价值，但最终还是需要更全面的规范，即正确性规范。例如，根据商定的正确性标准对软件库进行验证可能在广泛的领域中具有很高的价值。然而，要验证这种全面的规范，需要更重的分析，即定理证明。我们的建议侧重于开发工具，这些工具将支持分离逻辑中正确性规范的自动验证。特别是，我们将研究如何将轻量级和重型方法最佳地结合起来。我们提出了一种合作的方法，在这种方法中，各个技术结合它们的优势，但重要的是通过部分结果和失败的交流来弥补彼此的弱点。为了实现这种级别的合作，我们将使用一种称为证明计划的定理证明技术，该技术在构建协作推理工具方面具有经过验证的记录。我们计划将证明规划方法与由伦敦玛丽女王大学Peter O'Hearn研究小组开发的现有现成形状分析工具结合起来。请注意，我们的合作方法也将增强现有的形状分析工具，即使工具可扩展，从而更广泛地适用。如果我们的协作式集成是成功的，那么它将对降低开发高可靠性软件的成本产生重大影响。

项目成果

The CORE system: Animation and functional correctness of pointer programs

CORE系统：指针程序的动画和功能正确性

• DOI: 10.1109/ase.2011.6100132
• 发表时间: 2011
• 作者: Maclean E

Proof automation for functional correctness in separation logic

证明分离逻辑中功能正确性的自动化

• DOI: 10.1093/logcom/exu032
• 发表时间: 2016
• 期刊: Journal of Logic and Computation
• 影响因子: 0.7
• 作者: Maclean E