24.08.14 - 29.08.14, Seminar 14352

Next Generation Static Software Analysis Tools

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

Motivation

There has been tremendous progress in static software analysis over the last years, e.g., refined abstract interpretation methods, the advent of fast decision procedures like SAT and SMT solvers, new approaches like software (bounded) model checking or CEGAR, or new problem encodings. We are now close to integrating these techniques into every programmer's toolbox.

With this seminar, we want to bring together developers of software analysis tools and algorithms, including researchers working on the underlying decision procedures (e.g., SMT solvers), and people who are interested in applying these techniques (e.g. in the automotive or avionics industry).

The seminar offers the unique chance, by assembling the leading experts in these areas, to make a big step ahead in new, more powerful tools for static software analysis.

Current (academic) tools still suffer from some shortcomings:

  • Tools are not yet robust enough.
  • Scalability to large software packages is not yet sufficient.
  • Lack of standardized property specification and environment modeling constructs.
  • Differing interpretations of programming language semantics and missing interfaces between tools.
  • Lack of a comprehensive benchmark collection.

Additional questions to be discussed include:

  • What are the right logics for program verification, bug finding and software analysis (e.g., to handle universal quantification or to model main memory)?
  • Which decision procedures are most suitable for static software analysis? How can different procedures be combined? Which optimizations to general-purpose decision procedures (SAT/SMT/QBF) are possible in the context of software analysis?
  • What are the demands on software analysis tools from a practitioner's point of view?
  • How can scalability of these tools be improved?

This Dagstuhl seminar will be held concurrently with a second Dagstuhl seminar (14351), titled "Decision Procedures and Abstract Interpretation". The two seminars will be coordinated to some degree. The invitation lists will be disjoint, but it is likely that at least one joint activity will be carried out during the week.