Sagar Chaki

Samir Sapra, Marius Minea, Sagar Chaki, Arie Gurfinkel, Edmund M. Clarke, Proceedings of the 25th IFIP International Conference on Testing Software and Systems (ICTSS), page 283-289, November 13-15, 2013, Istanbul, Turkey.

Abstract: For statically typed languages, dynamic symbolic execution (also called concolic testing) is a mature approach to automated test generation. However, extending it to dynamic languages presents several challenges. Complex semantics, fragmented and incomplete type information, and calls to foreign functions lacking precise models make symbolic execution difficult. We propose a symbolic execution approach that mixes concrete and symbolic values and incrementally solves path constraints in search for alternate executions by lazily instantiating axiomatizations for called functions as needed. We present the symbolic execution model underlying this approach and illustrate the workings of our prototype concolic testing tool on an actual Python software package.