Projects

Inference Mechanisms for a Separation and Numerical Domain

The proliferation of software across all aspects of life means software failure can have significant economic and social impact. It is, therefore, highly desirable to be able to develop software that is formally verified as correct with respect to its expected specification. A key objective in this research is to find a systematic approach to abstraction construction in the combined domain, so appropriate abstractions can be employed by the inference process.

Inference Mechanisms for a Separation and Numerical Domain

The proliferation of software across all aspects of our life means that software failure can have significant economic and social impact. It is therefore highly desirable to be able to develop software that is formally verified as correct with respect to its expected specification. This has also been identified as a key objective in one of the UK Grand Challenges (GC6). Although research on formal verification has a long history, dating back to the 1960's, it remains a challenging problem to automatically verify programs written in mainstream imperative languages such as C, C++, C# and Java. This is in part due to the prolific use of (recursive) shared mutable data structures which are difficult to keep track of statically and in a precise and concise way.

The emergence of separation logic promotes scalable reasoning via explicit separation of structural properties over the memory heap where recursive data structures are dynamically allocated. Using separation logic, progress has recently been made on automated verification for pointer safety in the separation/shape domain. To verify the more general memory safety and functional correctness, it will require the combination of both separation (structural) and numerical (e.g. size) information. Therefore, advanced analysis and verification techniques are needed in the combined separation and numerical domain to verify memory safety and functional correctness. Nevertheless, this remains a clear challenge for program analysis research.

As a first step to tackle the challenge, Our recent development on program verification using a combined separation and numerical domain also allows user-specified inductive predicates to appear in program specifications for better expressivity. Based on this specification mechanism, a verification system called HIP/SLEEK has been built by the NUS team led by Prof Wei-Ngan Chin to conduct the automated verification and proof search. The experimental results have confirmed the viability of this approach. One issue with the current system is that it is a liability for the users to supply all loop invariants and method pre/post-conditions prior to the verification. This can be very demanding and challenging for the users.

As the second phase towards tackling the challenge, we propose to develop advanced inference mechanisms in the combined separation and numerical domain with user-defined predicates so that loop invariants and method pre/post-conditions can be automatically synthesised, where possible. Achieving this goal means that a much higher level of automation will be achieved, therefore a significant advance will be made in automated verification on memory safety and functional correctness.

A key objective in the proposed research is to find a systematic approach to abstraction construction in the combined domain, so that appropriate abstractions can be employed by the inference process. Abstractions are required in the analysis and verification for various reasons, such as termination and scalability. Appropriate abstraction mechanisms are crucial in maintaining a desirable scalability/precision trade-off. Apart from the abstraction mechanisms, we also intend to design analysis algorithms for loop invariant synthesis, method post-condition inference and method pre-condition discovery for the combined domain with arbitrary user-defined predicates. We will build a tool to implement these analyses and apply it to sizeable benchmark programs. As a challenging example, we will apply our tool for the verification of memory safety of a Linux kernel. Such a sizeable program can well be used to test the limit of our inference mechanisms.

We believe our research outcomes will further improve the level of automation, and therefore significantly extend the viability and applicability of automated verification on memory safety as well as functional correctness for substantial imperative programs.

Principal investigator: Professor Shengchao Qin
EPSRC Grant: EP/G042322/2
Starts: 01 June 2010
Ends: 30 September 2013

More details about the Inference Mechanisms for a Separation and Numerical Domain project