Workshop in Symbolic Execution
- Lecturers: Noam Rinetzky
- Time: Sunday, 09:00–11:00, Semester A, 2017/18
- Location: Kaplun 324
- Reception Hour: Set by Email
- Course Number: 0368-3526
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.
Announcements
- The first meeting of the workshop will take place on the second week of the semester, i.e., on 29/Oct/2017.
- Please read the paper "KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs" before the first meeting.
Tentative Schedule
- 29/10/2017 Introduction to symbolic execution + Home assignment
- 12/11/2017 Projects descriptions [PPTX] [PDF]
- 26/11/2017 Project selection and plan
- 24/12/2017 Progress report
- 21/01/2018 First phase submission
- 04/03/2018 Final project submission
- 15/03/2018 Project presentation