Dagstuhl Seminar 14352
Next Generation Static Software Analysis Tools
( Aug 24 – Aug 29, 2014 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/14352
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)
Coordinator
- Mana Taghdiri (KIT - Karlsruher Institut für Technologie, DE)
Contact
- Christina Schwarz (for administrative matters)
Schedule
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.
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.
Creative Commons BY 3.0 Unported license
Patrick Cousot and Daniel Kroening and Carsten Sinz
- Roberto Bagnara (BUGSENG - Parma, IT & University of Parma, IT) [dblp]
- Dirk Beyer (Universität Passau, DE) [dblp]
- Mehdi Bouaziz (ENS - Paris, FR) [dblp]
- Patrick Cousot (ENS - Paris, FR) [dblp]
- Tomasz Dudziak (Universität des Saarlandes, DE) [dblp]
- David Faragó (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Christian Ferdinand (AbsInt - Saarbrücken, DE) [dblp]
- Jérôme Feret (ENS - Paris, FR) [dblp]
- Marcelo Frias (University of Buenos Aires, AR) [dblp]
- Vijay Ganesh (University of Waterloo, CA) [dblp]
- Roberto Giacobazzi (University of Verona, IT) [dblp]
- Christoph Gladisch (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Udo Gleich (Daimler R&D - Ulm, DE)
- Manuel Hermenegildo (IMDEA Software - Madrid, ES) [dblp]
- Ralf Huuck (Data61 / NICTA - Sydney, AU) [dblp]
- Daniel Kroening (University of Oxford, GB) [dblp]
- K. Rustan M. Leino (Microsoft Corporation - Redmond, US) [dblp]
- Francesco Logozzo (Microsoft Corporation - Redmond, US) [dblp]
- Peter Müller (ETH Zürich, CH) [dblp]
- Filip Niksic (MPI-SWS - Kaiserslautern, DE) [dblp]
- Andreas Podelski (Universität Freiburg, DE) [dblp]
- Hendrik Post (Robert Bosch GmbH - Stuttgart, DE) [dblp]
- Francesco Ranzato (University of Padova, IT) [dblp]
- Xavier Rival (ENS - Paris, FR) [dblp]
- Helmut Seidl (TU München, DE) [dblp]
- Carsten Sinz (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Michael Tautschnig (Queen Mary University of London, GB) [dblp]
- Shmuel Tyszberowicz (Academic College of Tel Aviv, IL) [dblp]
- Caterina Urban (ENS - Paris, FR) [dblp]
- Tomas Vojnar (Brno University of Technology, CZ) [dblp]
- Milena Vujosevic-Janicic (University of Belgrade, RS) [dblp]
- Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
Classification
- semantics / formal methods
- software engineering
- verification / logic
Keywords
- Software quality
- bug finding
- verification
- decision procedures
- SMT/SAT solvers
