27.10.14 - 30.10.14, Seminar 14442

Symbolic Execution and Constraint Solving

Diese Seminarbeschreibung wurde vor dem Seminar auf unseren Webseiten veröffentlicht und bei der Einladung zum Seminar verwendet.

Motivation

Symbolic execution has garnered a lot of attention in recent years as an effective technique for generating high-coverage test suites, finding deep errors in complex software applications, and more generally as one of the few techniques that is useful across the board in myriad software engineering applications. While key ideas behind symbolic execution were introduced more than three decades ago, it was only recently that these techniques became practical as a result of significant advances in constraint satisfiability and scalable combinations of concrete and symbolic execution. The result has been an explosion in applications of symbolic execution techniques in software engineering, security, formal methods and systems research. Furthermore, researchers are combining symbolic execution with traditional program analysis techniques in novel ways to address longstanding software engineering problems. This in turn has led to rapid developments in both constraint solvers and symbolic execution techniques, necessitating an in-depth exchange of ideas between researchers working on solvers and symbolic techniques, best accomplished through dedicated workshops. Hence, the goal of this seminar is to bring together the leading researchers in the fields of symbolic execution and constraint solving, foster greater communication, exchange ideas about new research directions and feedback from solver users to developers. In the following, we highlight the main challenges in modern symbolic execution techniques and constraint solving that will be addressed during the seminar from different research perspectives:

  • How to cope with path explosion?
  • How to exploit the type of constraints generated during the symbolic execution of real programs?
  • How to design and implement solvers that can handle rich constraints generated through symbolic execution and program analysis?
  • How to enable precise analysis of program statements?
  • How to extend symbolic execution to efficiently handle concurrent programs?

Symbolic execution plays a key role in the work on several different communities - particularly software engineering, testing, verification, computer systems and software security - as evidenced by the large number of publications on this topic in top venues in each of these areas, such as ICSE, FSE, ASE (software engineering); OSDI, EuroSys, ICDCS, IPSN, ASPLOS (systems); ISSTA, ICST (testing); CAV, HVC (verification); and CCS, IEEE Security and Privacy (security). One of the core goals of the seminar is to bring together these many different communities that work on symbolic execution techniques, communities which unfortunately rarely talk to each other. We believe that the exchange of ideas between these different communities - each with their own methods and perspectives on the field - would help accelerate the future development of symbolic execution and constraint solving techniques. In terms of concrete outcomes, we believe the seminar is likely to lead to several collaboration projects both between members of the same community, but also between members of different communities that work on the same problems in the symbolic execution and constraint solving areas.