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..