Prototyping symbolic execution engines for interpreted languages

Stefan Bucur, Johannes Kinder, George Candea

Research output: Chapter in Book/Report/Conference proceedingConference contribution

188 Downloads (Pure)


Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways.

We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called Chef) for turning a vanilla interpreter into a sound and complete symbolic execution engine. Chef symbolically executes the target program by symbolically executing the interpreter's binary while exploiting inferred knowledge about the program's high-level structure.

Using Chef, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. Chef-produced engines are up to 1000 times more performant than if directly executing the interpreter symbolically without Chef.
Original languageEnglish
Title of host publicationASPLOS '14
Subtitle of host publicationProceedings of the 19th international conference on Architectural support for programming languages and operating systems
Number of pages16
ISBN (Electronic)978-1-4503-2305-5
Publication statusPublished - Feb 2014

Cite this