| 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: |
|
| 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: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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
|
|
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.imperial.ac.uk |