Research Perspectives - Tools for Visualisation of Portfolios
EPSRC logo

EPSRC Database


Source RCUK EPSRC Data

EP/J00636X/1 - Testing, Verifying, and Generating Software Patches Using Dynamic Symbolic Execution

Research Perspectives grant details from EPSRC portfolio

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

Dr C Cadar EP/J00636X/1 - Testing, Verifying, and Generating Software Patches Using Dynamic Symbolic Execution

Principal Investigator - Dept of Computing, Imperial College London

Scheme

Standard Research

Research Areas

Software Engineering Software Engineering

Verification and Correctness Verification and Correctness

Collaborators

Maxeler Technologies Maxeler Technologies

Start Date

05/2012

End Date

05/2015

Value

£287,184

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

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.

Structured Data / Microdata


Grant Event Details:
Name: Testing, Verifying, and Generating Software Patches Using Dynamic Symbolic Execution - EP/J00636X/1
Start Date: 2012-05-31T00:00:00+00:00
End Date: 2015-05-30T00:00:00+00:00

Organization: Imperial College London

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