Paper Info
Title
Compositional Symbolic Execution Using Fine-Grained Summaries
Abstract
Compositional symbolic execution has been proposed as a way to increase the efficiency of symbolic execution. Essentially, when a function is symbolically executed, a summary of the path that was executed is stored. This summary records the precondition and post condition of the path, and on subsequent calls that satisfy that precondition, the corresponding post condition can be returned instead of executing the function again. However, using functions as the unit of summarisation leaves the symbolic execution tool at the mercy of a program designer, essentially resulting in an arbitrary summarisation strategy. In this paper, we explore the use of fine-grained summaries, in which blocks within functions are summarised. We propose three types of summarisation and demonstrate how to generate these. At such a fine-grained level, symbolic execution of a path effectively becomes the concatenation of the summaries along that path. Using a prototype symbolic execution tool, we perform a preliminary experimental evaluation of our summary approaches, demonstrating that they can improve the speed of symbolic execution by reducing the number of calls sent to the underlying constraint solver.
Year
DOI
Venue
2015
10.1109/ASWEC.2015.32
ASWEC
Keywords
Field
DocType
Test generation,path explosion,constraint solving
The Symbolic,Information system,Programming language,Computer science,Precondition,Theoretical computer science,Constraint satisfaction problem,Concolic testing,Symbolic execution,Concatenation,Symbolic trajectory evaluation
Conference
ISSN
Citations 
PageRank 
1530-0803
2
0.38
References 
Authors
25
3
Name
Order
Citations
PageRank
Yude Lin120.72
Tim Miller2778.34
Harald Søndergaard385879.52