Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)

Authors Patrick Cousot, Daniel Kroening, Carsten Sinz and all authors of the abstracts in this report



PDF
Thumbnail PDF

File

DagRep.4.8.107.pdf
  • Filesize: 0.96 MB
  • 19 pages

Document Identifiers

Author Details

Patrick Cousot
Daniel Kroening
Carsten Sinz
and all authors of the abstracts in this report

Cite As Get BibTex

Patrick Cousot, Daniel Kroening, and Carsten Sinz. Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352). In Dagstuhl Reports, Volume 4, Issue 8, pp. 107-125, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/DagRep.4.8.107

Abstract

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?

Subject Classification

Keywords
  • Software quality
  • Bug finding
  • Verification
  • Decision procedures
  • SMT/SAT solvers

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail