Details of Grant 

EPSRC Reference:	EP/G042322/1
Title:	Inference Mechanisms for a Separation and Numerical Domain
Principal Investigator:	Qin, Professor S
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	Durham, University of
Scheme:	Standard Research
Starts:	01 October 2009	Ends:	31 May 2010	Value (£):	395,662
EPSRC Research Topic Classifications:	Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 29 Jan 2009 ICT Prioritisation Panel (January 2009) Announced
Summary on Grant Application Form
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 to conduct the automated verification and proof search. Our 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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website: