Cooperative Reasoning for 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.