CORE: Cooperative Reasoning for Automatic Software Verification

Project Team


The proliferation of software across all aspects of modern life means that software failures can have significant economic and 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 and distinguished history, dating back over fifty years. What has remained 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 industry as well as academia. A significant recent development has been Separation Logic, a logic which promotes scalable reasoning for pointer programs. Pointers are a powerful and widely used programming mechanism, but developing and maintaining correct pointer 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 content of 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 called for, i.e. correctness specifications. For instance, the verification of software libraries against agreed correctness standards could prove highly valuable across a wide range of sectors. However, to verify such comprehensive specifications requires more heavy-weight analysis, i.e. theorem proving.

Our project focuses on the development of tools which will support the automatic verification of correctness specifications within 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, and in particular cooperative software verification tools, see NuSPADE. 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 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. A pdf version of the full project proposal can be accessed here .

Further details can be obtained from Andrew Ireland, Dependable Systems Group, School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, EH14 4AS, UK [, +44 (0)131 451 3409 ]

| Publications | Presentations | CORE System |