Compositional Symbolic Execution Using Fine-Grained Summaries

8 years 4 days ago

Download people.eng.unimelb.edu.au

Abstract—Compositional symbolic execution has been proposed as a way to increase the efﬁciency 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 ﬁne-grained summaries, in which blocks within functions are summarised. We propose three types of summarisation and demonstrate how to generate these. At such a ﬁne-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...

Yude Lin, Tim Miller, Harald Søndergaard

Real-time Traffic