Details of Grant 

EPSRC Reference:	EP/E053041/1
Title:	Scalable Program Analysis for Software Verification
Principal Investigator:	YANG, Professor H
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	Queen Mary University of London
Scheme:	Advanced Fellowship
Starts:	01 October 2007	Ends:	01 May 2011	Value (£):	437,666
EPSRC Research Topic Classifications:	Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:	Panel Date Panel Name Outcome 24 Apr 2007 ICT Fellowships 2007 - Interviews FinalDecisionYetToBeMade 29 Mar 2007 ICT Fellowships Sift Panel InvitedForInterview
Summary on Grant Application Form
Recent years have seen a renaissance in automatic program verification, based on advances in program analysis (abstract interpretation).Tools such as Microsoft's Static Driver Verifiercan automatically verify certain lightweight properties (e.g., protocol properties)of interfaces between program components.There is, though, a fundamental problem:Scalable methods are lacking.Current tools are based on a closed world assumption,where a complete program is available,and they work over a system's entire global state.This lack of modularity impedes scalability, and wider applicability. This research proposes an attack on the scalability problem.Our thesis is that progress in three directions, localization,isolation and generalization, can lead to much more scalable analyses.The idea of the first two of these isto reduce the cost for analyzing each component once,while the third aims to ensure thatone analysis result of a program component can be reused in manydifferent contexts. We will develop a general framework and concreteinstances of analyses that achieve these three goals.We will test our ideas by developing prototype toolsthat we will apply to widely-used open-source infrastructure software,such as network software and operating system components.Scalability is the core problem in the automatic verification of software.Success on the problems in this research would have a majorimpact on the use of automatic techniques for theanalysis and verification of significant, real-world code.
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: