10.4230/LIPICS.RTA.2011.41
Falke, Stephan
Stephan
Falke
Kapur, Deepak
Deepak
Kapur
Sinz, Carsten
Carsten
Sinz
Termination Analysis of C Programs Using Compiler Intermediate Languages
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
termination analysis; C programs; compiler intermediate languages
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
2011
2011-04-26
2011-04-26
2011-04-26
en
urn:nbn:de:0030-drops-31232
10.4230/LIPIcs.RTA.2011
978-3-939897-30-9
1868-8969
10.4230/LIPIcs.RTA.2011
LIPIcs, Volume 10, RTA 2011
22nd International Conference on Rewriting Techniques and Applications (RTA'11)
2013
10
7
41
50
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
10
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
10 pages
632169 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), pages 41-50