wiki:summer-projects/2011-dise

JPF-Regression

Abstract

Directed Incremental Symbolic Execution (DiSE) is a technique for detecting and characterizing the effects of changes between two related program versions. The idea in DiSE is to combine the efficiencies of static analysis techniques with the precision of symbolic execution to explore program execution paths and generate path conditions affected by the differences.

Contact

student: Josh Branchaud

mentor: Neha Rungta (neha.s.rungta@…)

co-mentor: Suzette Person (suzette.person@…)

Repository

http://babelfish.arc.nasa.gov/hg/jpf/jpf-regression

Description

DiSE uses static analysis techniques that compute program difference information with symbolic execution. The path conditions computed by DiSE then characterize the differences between two related program versions. The essence of symbolic execution is that it abstracts the semantics of program behaviors by generating constraints on program inputs. The goal of DiSE is to direct symbolic execution on a modified program version to explore path conditions that may be affected by the changes. Affected path conditions can be solved to generate values for the variables which, when used to execute the program, exhibit the affected program behaviors. The results of DiSE can be then used by subsequent program analysis techniques to focus on only the program behaviors that are affected by the changes to the program.

Details of DiSE can be read in the PLDI 2011 paper, Directed Incremental Symbolic Execution.

Last modified 6 years ago Last modified on 02/19/2012 09:38:10 AM