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 postcondition of the path, and on subsequent calls that satisfy that precondition, the corresponding postcondition 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 per...

• Type: Journal
• Year: 2015
• Where: ASWEC
• Authors: Yude Lin, Tim Miller, Harald Søndergaard
• Keywords: ASWEC 2015, Software Engineering