DROPS

Document

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.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}
}

Document

DOI: 10.4230/LIPIcs.RTA.2011.41

Termination Analysis of C Programs Using Compiler Intermediate Languages

Authors: Stephan Falke, Deepak Kapur, and Carsten Sinz

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract

Modeling the semantics of programming languages like C for the automated termination analysis of programs is a challenge if complete coverage of all language features should be achieved. On the other hand, low-level intermediate languages that occur during the compilation of C programs to machine code have a much simpler semantics since most of the intricacies of C are taken care of by the compiler frontend. It is thus a promising approach to use these intermediate languages for the automated termination analysis of C programs. In this paper we present the tool KITTeL based on this approach. For this, programs in the compiler intermediate language are translated into term rewrite systems (TRSs), and the termination proof itself is then performed on the automatically generated TRS. An evaluation on a large collection of C programs shows the effectiveness and practicality of KITTeL on "typical" examples.

Cite as

Stephan Falke, Deepak Kapur, and Carsten Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 41-50, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{falke_et_al:LIPIcs.RTA.2011.41,
  author =	{Falke, Stephan and Kapur, Deepak and Sinz, Carsten},
  title =	{{Termination Analysis of C Programs Using Compiler Intermediate Languages}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{41--50},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.41},
  URN =		{urn:nbn:de:0030-drops-31232},
  doi =		{10.4230/LIPIcs.RTA.2011.41},
  annote =	{Keywords: termination analysis; C programs; compiler intermediate languages}
}

Search Results

Documents authored by Sinz, Carsten

Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)

Abstract

Cite as

Termination Analysis of C Programs Using Compiler Intermediate Languages

Abstract

Cite as

Thanks for your feedback!

Could not send message