Research Perspectives - Tools for Visualisation of Portfolios
EPSRC logo

EPSRC Database


Source RCUK EPSRC Data

EP/E053041/2 - Scalable Program Analysis for Software Verification

Research Perspectives grant details from EPSRC portfolio

http://www.researchperspectives.org/gow.grants/grant_EPE0530412.png

Dr H YANG EP/E053041/2 - Scalable Program Analysis for Software Verification

Principal Investigator - Computer Science, University of Oxford

Scheme

Advanced Fellowship

Research Areas

Verification and Correctness Verification and Correctness

Start Date

05/2011

End Date

09/2012

Value

£120,683

Similar Grants

Automatic generation of similar EPSRC grants

Similar Topics

Topic similar to the description of this grant

Grant Description

Summary and Description of the grant

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.

Structured Data / Microdata


Grant Event Details:
Name: Scalable Program Analysis for Software Verification - EP/E053041/2
Start Date: 2011-05-01T00:00:00+00:00
End Date: 2012-09-30T00:00:00+00:00

Organization: University of Oxford

Description: 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 ...