Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Demand-Driven Compositional Symbolic Execution

Saswat Anand, Patrice Godefroid, and Nikolai Tillmann

Abstract

We discuss how to perform symbolic execution of large programs in a manner that is both compositional (hence more scalable) and demand-driven. Compositional symbolic execution means finding feasible interprocedural program paths by composing symbolic executions of feasible intraprocedural paths. By demand-driven, we mean that as few intraprocedural paths as possible are symbolically executed in order to form an interprocedural path leading to a specific target branch or statement of interest (like an assertion). A key originality of this work is that our demand-driven compositional interprocedural symbolic execution is performed entirely using first-order logic formulas solved with an off-the-shelf SMT (Satisfiability-Modulo-Theories) solver – no procedure in-lining or custom algorithm is required for the interprocedural part. This allows a uniform and elegant way of summarizing procedures at various levels of detail and of composing those using logic formulas. We have implemented a prototype of this novel symbolic execution technique as an extension of Pex, a general automatic testing framework for .NET applications. Preliminary experimental results are encouraging. For instance, our prototype was able to generate tests triggering assertion violations in programs with large numbers of program paths that were beyond the scope of non-compositional test generation.

Details

Publication typeInproceedings
Published inProc. International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008
URLhttp://dx.doi.org/10.1007/978-3-540-78800-3_28
Pages367-381
Volume4963
SeriesLecture Notes in Computer Science
PublisherSpringer Verlag

Previous versions

Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. Demand-Driven Compositional Symbolic Execution, Microsoft, October 2007.

> Publications > Demand-Driven Compositional Symbolic Execution