1 Search Results for "Sinz, Daniel"

Document
DOI: 10.4230/DagRep.4.8.107
Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)

Authors: Patrick Cousot, Daniel Kroening, and Carsten Sinz

Published in: Dagstuhl Reports, Volume 4, Issue 8 (2015)

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?
Cite as

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)

Copy BibTex To Clipboard

@Article{cousot_et_al:DagRep.4.8.107,
  author =	{Cousot, Patrick and Kroening, Daniel and Sinz, Carsten},
  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 =	{Cousot, Patrick and Kroening, Daniel and Sinz, Carsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.8.107},
  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}
}
  • Refine by Author
  • 1 Cousot, Patrick
  • 1 Kroening, Daniel
  • 1 Sinz, Carsten

  • Refine by Classification

  • Refine by Keyword
  • 1 Bug finding
  • 1 Decision procedures
  • 1 SMT/SAT solvers
  • 1 Software quality
  • 1 Verification

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2014

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact