License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.4.8.107
URN: urn:nbn:de:0030-drops-48203
Go back to Dagstuhl Reports

Cousot, Patrick ; Kroening, Daniel ; Sinz, Carsten
Weitere Beteiligte (Hrsg. etc.): Patrick Cousot and Daniel Kroening and Carsten Sinz

Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)

dagrep_v004_i008_p107_s14352.pdf (1.0 MB)


There has been tremendous progress in static software analysis over the last years with, for example, 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.

The aim of the seminar was 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 offered the unique chance, by assembling the leading experts in these areas, to make a big step ahead towards new, more powerful tools for static software analysis.

Current (academic) tools still suffer from some shortcomings:
- Tools are not yet robust enough or support only a subset of a programming language's features.
- Scalability to large software packages is not yet sufficient.
- There is a lack of standardized property specification and environment modeling constructs, which makes exchange of analysis results more complicated than necessary.
- Differing interpretations of programming language semantics by different tools lead to limited trust in analysis results.
- Moreover, a comprehensive benchmark collection to compare and evaluate tools is missing.

Besides these application-oriented questions, further, more fundamental questions have also been topics of the seminar:

- What are the right logics for program verification, bug finding and software analysis?
- How can we handle universal quantification? And how to model main memory and complex data structures?
- 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?

BibTeX - Entry

  author =	{Patrick Cousot and Daniel Kroening and Carsten Sinz},
  title =	{{Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)}},
  pages =	{107--125},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{8},
  editor =	{Patrick Cousot and Daniel Kroening and Carsten Sinz},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-48203},
  doi =		{10.4230/DagRep.4.8.107},
  annote =	{Keywords: Software quality, Bug finding, Verification, Decision procedures, SMT/SAT solvers}

Keywords: Software quality, Bug finding, Verification, Decision procedures, SMT/SAT solvers
Collection: Dagstuhl Reports, Volume 4, Issue 8
Issue Date: 2014
Date of publication: 09.12.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI