Seminar on Programming Languages and Program Analysis

Symbolic Execution

• Lecturer: Noam Rinetzky
• Semester: B
• Time: Sunday, 09:00–11:00, 2017/18
• Place: Orenstein 102
• Course Number: 0368–3181

Topic

In this seminar we will discuss classic and state-of-the-art papers regarding symbolic execution.

Symbolic Execution (description taken from "Symbolic execution for software testing: three decades later ©ACM 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.

Requirements

• Give a 70-80 minutes talk about his or hers assigned topic (one or more research papers).
• Answer students questions during the talk.
• Lead a summary discussion.
• Say something original (i.e., not written in the paper) about the topic. For example:
  • Download and execute two implementations of the described algorithm and evaluate them.
  • Extend the discussion regarding a particularly close related work.
  • Make an interesting connection to a topic discussed in a previous talk.
  • Describe a personal expereicne with using the discussed technique (or a simialr one) at work.
• Write a short (1 page) summary about the discussed topic, the original contribution, and the main points that came out during the discussion.
• Actively participate in the discussions led by other students.

Admin

• The talk can be given either in Hebrew or in English. The slides and the summary should be written in English.
• You are expected to be present in every lesson, unless coordinated beforehand with the lecturer.
• Use the seminar's themes for your presentation and summary: [Presentation theme] [Summary theme].
• Name your presentation and summary using the seminar's naming conventions, e.g.,
  • seminar1718b-lec-Num-presentation-firstname-secondname.pptx
  • seminar1718b-lec-Num-summary-firstname-secondname.docx
• Mathematical fonts for Powerpoint and Word can be found here.

Schedule