EPSRC logo

Details of Grant 

EPSRC Reference: EP/J00636X/1
Title: Testing, Verifying, and Generating Software Patches Using Dynamic Symbolic Execution
Principal Investigator: Cadar, Professor C
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Maxeler Technologies Ltd
Department: Computing
Organisation: Imperial College London
Scheme: Standard Research
Starts: 31 May 2012 Ends: 31 July 2015 Value (£): 287,184
EPSRC Research Topic Classifications:
Artificial Intelligence Software Engineering
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
06 Sep 2011 EPSRC ICT Responsive Mode - Sep 2011 Announced
Summary on Grant Application Form
A large fraction of the costs of developing and maintaining software is associated with detecting and fixing software errors. As a result, the last decade has seen a sustained research effort directed toward designing and developing techniques for automatically detecting software errors, with some of these techniques making their way into commercial and open-source tools. However, detecting an error is only the first step toward fixing it. In fact, many known errors remain unpatched due to the high cost required to diagnose and repair them, combined with the fear that patches are more likely to introduce failures compared to other types of code changes.

The goal of this research project is to address both of these problems, by devising novel techniques based on dynamic symbolic execution for:

(1) automatically testing and verifying the correctness of software patches, and

(2) (semi-)automatically generating candidate patches for software bugs.

The strength of dynamic symbolic execution lies in its ability to precisely model the behaviour of program paths using mathematical constraints. However, the cost associated with this level of precision is poor scalability. The number of paths in a program is usually exponential in the number of branches, which makes it difficult to scale the analysis to very large programs. However, by focusing the analysis on the incremental changes introduced by program patches, we hope to significantly reduce the cost of symbolic execution and significantly increase its applicability in practice. Furthermore, the ability to check software patches opens up the possibility of performing patch generation in an automatic or semi-automatic fashion. In particular, starting from the mathematical constraints gathered from a buggy execution path -- and with the potential addition of a manually-written patch template -- we plan to design techniques for generating a set of candidate patches resembling the ones that would be generated manually by developers.
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
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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.imperial.ac.uk