License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.41
URN: urn:nbn:de:0030-drops-31232
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3123/
Go to the corresponding LIPIcs Volume Portal

Falke, Stephan ; Kapur, Deepak ; Sinz, Carsten

Termination Analysis of C Programs Using Compiler Intermediate Languages

pdf-format:
16.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{falke_et_al:LIPIcs:2011:3123,
  author =	{Stephan Falke and Deepak Kapur and Carsten Sinz},
  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 =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3123},
  URN =		{urn:nbn:de:0030-drops-31232},
  doi =		{10.4230/LIPIcs.RTA.2011.41},
  annote =	{Keywords: termination analysis; C programs; compiler intermediate languages}
}

Keywords: termination analysis; C programs; compiler intermediate languages
Collection: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI