Cooperative Reasoning for Automatic Software Verification

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

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.