MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

MultiSE: Multi-Path Symbolic Execution using Value Summaries

Koushik Sen
UC Berkeley
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Thursday, 30 October 2014
16:00
60 Minutes
G26
111
Kaiserslautern

Abstract

Dynamic symbolic execution (DSE) has been proposed to effectively generate test inputs for real-world programs. Unfortunately, DSE techniques do not scale well for large realistic programs, because often the number of feasible execution paths of a program increases exponentially with the increase in the length of an execution path.

In this paper, we propose MultiSE, a new technique for merging states incrementally during symbolic execution, without using auxiliary variables. The key idea of MultiSE is based on an alternative representation of the state, where we map each variable, including the program counter, to a set of guarded symbolic expressions called a value summary. MultiSE has several advantages over conventional DSE and existing state merging techniques: value summaries enable sharing of symbolic expressions and path constraints along multiple paths and thus avoid redundant execution. MultiSE does not introduce auxiliary symbolic variables, which enables it to 1) make progress even when merging values not supported by the constraint solver, 2) avoid expensive constraint solver calls when resolving function calls and jumps, and 3) carry out most operations concretely. Moreover, MultiSE updates value summaries incrementally at every assignment instructions, which makes it unnecessary to identify the join points and to keep track of variables to merge at join points.

We have implemented MultiSE for JavaScript programs in a publicly available open-source tool. Our evaluation of MultiSE on several programs shows that MultiSE can run significantly faster than traditional dynamic symbolic execution and save substantial number of state merges compared to existing state merging techniques.

Contact

Susanne Girard
--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
002
passcode not visible
logged in users only

Susanne Girard, 10/23/2014 15:05
Susanne Girard, 10/22/2014 13:56 -- Created document.