| EPSRC Reference: |
EP/E053041/2 |
| Title: |
Scalable Program Analysis for Software Verification |
| Principal Investigator: |
YANG, Professor H |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
Advanced Fellowship |
| Starts: |
01 May 2011 |
Ends: |
30 September 2012 |
Value (£): |
120,683
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
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: |
http://www.ox.ac.uk |