Guowei Yang, Sarfraz Khurshid, and Corina S. Păsăreanu

University of Texas at Austin, USA; CMU, USA; NASA Ames Research Center, USA

Track: Formal Tool Demonstrations
Session: Formal Demonstrations 2
This tool paper presents a tool for performing memoized symbolic execution (Memoise), an approach we developed in previous work for more efficient application of symbolic execution. The key idea in Memoise is to allow re-use of symbolic execution results across different runs of symbolic execution without having to re-compute previously computed results as done in earlier approaches. Specifically, Memoise builds a trie-based data structure to record path exploration information during a run of symbolic execution, optimizes the trie for the next run, and re-uses the resulting trie during the next run. Our tool optimizes symbolic execution in three standard scenarios where it is commonly applied: iterative deepening, regression analysis, and heuristic search. Our tool Memoise builds on the Symbolic PathFinder framework to provide more efficient symbolic execution of Java programs and is available online for download. The tool demonstration video is available at http://www.youtube.com/watch?v=ppfYOB0Z2vY&feature=plcp.