The Blavatnik School of Computer Science TAU
Noam Rinetzky

Workshop in Symbolic Execution

Workshop description

Symbolic Execution (description taken from "Symbolic execution for software testing: three decades later", by Cristian Cadar and Koushik Sen, CACM 2013): Symbolic execution has garnered a lot of attention in recent years as an effective technique for generating high-coverage test suites and for finding deep errors in complex software applications. While the key idea behind symbolic execution was introduced more than three decades ago, it has only recently been made practical, as a result of signi cant advances in constraint satis ability, and of more scalable dynamic approaches that combine concrete and symbolic execution.

Symbolic execution is typically used in software testing to explore as many different program paths as possible in a given amount of time, and for each path to generate a set of concrete input values exercising it, and check for the presence of various kinds of errors including assertion violations, uncaught exceptions, security vulnerabilities, and memory corruption. The ability to generate concrete test inputs is one of the major strengths of symbolic execution: from a test generation perspective, it allows the creation of high-coverage test suites, while from a bug-finding perspective, it provides developers with a concrete input that triggers the bug, which can be used to con rm the error independently of the symbolic execution tool that generated it.

Furthermore, note that in terms of finding errors on a given program path, symbolic execution is much more powerful than traditional dynamic execution techniques such as those implemented by popular tools like Valgrind or Purify, because it has the ability to find a bug if there are any buggy inputs on that path, rather than depending on having a concrete input that triggers the bug. Finally, unlike other program analysis techniques, symbolic execution is not limited to finding generic errors such as buffer overflows, but can reason about higher-level program properties, such as complex program assertions.

In this workshop, we will design and implement symbolic execution tools.

[PPTX] [PDF]

Announcements

Tentative Schedule