http://www.dagstuhl.de/14352

August 24 – 29 , 2014, Dagstuhl Seminar 14352

Next Generation Static Software Analysis Tools

Organizers

Patrick Cousot (ENS – Paris, FR)
Klaus Havelund (NASA – Pasadena, US)
Daniel Kroening (University of Oxford, GB)
Carsten Sinz (KIT – Karlsruher Institut für Technologie, DE)

Coordinators

Mana Taghdiri (KIT – Karlsruher Institut für Technologie, DE)


1 / 2 >

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 4, Issue 8 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Schedule [pdf]

Summary

Software errors are still a widespread plague. They manifest themselves, e.g., in program crashes, malfunction, incorrect behavior, or security vulnerabilities. Even software that has been in use for decades and has been deployed to millions of users (e.g., the compression library zlib) still contains flaws that are revealed only now and have to be fixed. Both in academia and industry considerable effort has been undertaken to develop tools and methodologies to obtain fault-free software. Nowadays, static analysis tools, which search for program errors without running the software, have reached a state where they are, in some industries (e.g., the automotive or avionics industry), already part of the standard software development and quality assurance process (with tools and companies like, e.g., Polyspace, Coverity, KlocWork, AbsInt, or Astrée). And although these tools can help finding residual errors more quickly, they still suffer from some shortcomings:

  • Lack in precision. For a certain fraction of program locations in the source code it cannot be decided whether there is an error or not. Such "undecided cases" require (often time-consuming) manual rework, limiting the value of such tools.
  • Due to the manual effort required, static software analysis tools have not yet made their way to mainstream software development (besides industries, where software reliability is indispensable and considerable amounts of time and money are spent on quality assurance).

Over the last years, software analysis tools based on abstract interpretation have been refined and tools based on new core formalisms, such as model checking, have gained traction, mainly in the form of two key methods: counterexample-guided abstraction refinement (CEGAR), and bounded model checking (BMC). The success of these new tools was, to a substantial part, enabled by the enormous progress that was made on the underlying logical decision procedures (SAT and SMT solvers). New software analysis tools based on these techniques come with considerably improved precision (less false positives), but they are still not competitive with tools based on abstract interpretation with respect to scalability. Also, they are rarely used in industrial software development projects so far.

With this seminar we believe that we were able to stimulate further progress in this field by intensifying the collaboration between (a) researchers on new static software analysis tools, (b) scientists working on improved high-performance decision procedures, and (c)practitioners, who know what is needed in industry and which kind of software analysis tools are accepted by developers and which are not.

The Dagstuhl Seminar was attended by participants from both industry and academia. It included presentations on a wide range of topics such as:

  • Recent trends in static analysis, consisting of new algorithms and implementation techniques.
  • New decision procedures for software analysis, for example, to analyze programs with complex data structures.
  • Industrial case studies: What are the problems industrial users of static analysis tools are facing?
  • Experience reports and statements on current challenges.

The first day of the seminar started with an introduction round, in which each participant shortly presented his research interests. As the seminar was held concurrently with a second, closely related Dagstuhl Seminar on "Decision Procedures and Abstract Interpretation" (14351), the introductory session was held jointly by both seminars. Four overview talks were also organized jointly by both seminars, and were given by Thomas Reps, Patrick Cousot, Vijay Ganesh, and Francesco Logozzo.

There was also a tool demonstration session on Thursday afternoon, in which seven tools were presented (15 minutes each).

In further talks of the seminar young as well as senior researchers presented on-going and completed work. Tool developers and participants from industry reflected on current challenges in the realm of software analysis.

The seminar was concluded with a panel discussion about the current challenges of static software analysis for industrial application (see Sec. 5 for an extended exposition of the panel discussion).

We expect that with this Dagstuhl Seminar we were able to make a step forward towards bringing static software analysis tools to every programmer's workbench, and therefore, ultimately, improve software quality in general.

License
Creative Commons BY 3.0 Unported license
Patrick Cousot and Daniel Kroening and Carsten Sinz

Classification

  • Semantics / Formal Methods
  • Software Engineering
  • Verification / Logic

Keywords

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

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.