The Blavatnik School of Computer Science TAU
Noam Rinetzky

Seminar on Programming Languages and Program Analysis

Symbolic Execution Tools for Software Testing

Announcements

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

Admin

Schedule

  1. Topic: Overview
  2. Topic: Concrete testing tools
    • Date: 29/Oct/2017
    • Presenter: Ran Amar
    • Papers: [21], [28]
    • Presentation:
  3. Topic: Constraint solving
  4. Topic: Classic symbolic execution
    • Date: 12/Nov/2017
    • Presenter: Ofek Tamir
    • Papers: [23], [6], [12]
    • Presentation:
  5. Topic: Concolic execution
    • Date: Ilor Ifrah
    • Presenter: 19/Nov/2017
    • Papers: [19], [35]
    • Presentation:
  6. Topic: Execution-generated testing (EGT)
    • Date: 26/Nov/2017
    • Presenter: Neta Golan
    • Papers: [9], [10], [8]
    • Presentation:
  7. Topic: Search heuristics I
    • Date: 3/Dec/2017
    • Presenter: Ami Tahan
    • Papers: [7], [26]
    • Presentation:
  8. Topic: Search heuristics II
  9. Topic: Chopped Symbolic Execution
    • Date: 24/Dec/2017
    • Presenter: David Trabish
    • Papers: ICSE'17
    • Presentation:
  10. Topic: Symbolic Execution with Summaries
    • Date: 31/Dec/2017
    • Presenter: Omer Anson
  11. NO LESSON
    • Date: 7/Jan/2018
  12. Topic: Tools
    • Date: 14/Jan/2018
    • Presenter:
    • Papers: S2E, Calysto, [25]
    • Presentation:

[N] is the citation number in Symbolic execution for software testing: three decades later