CORE: Cooperative Reasoning for Automatic Software Verification |
Project Team
Overview
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
[ a.ireland@hw.ac.uk, +44 (0)131 451 3409 ]