Termination Analysis of C Programs Using Compiler Intermediate Languages

DOI10.4230/LIPIcs.RTA.2011.41zbMath1236.68040OpenAlexW2258703518MaRDI QIDQ5389070

Carsten Sinz, Deepak Kapur, Stephan Falke

Publication date: 24 April 2012

Full work available at URL: http://subs.emis.de/LIPIcs/frontdoor_633b.html

zbMATH Keywords

termination analysisC programscompiler intermediate languages

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Related Items (11)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Loop detection by logically constrained term rewriting ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution ⋮ Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution ⋮ System-level state equality detection for the formal dynamic verification of legacy distributed applications ⋮ Proving Termination Through Conditional Termination ⋮ Automatic complexity analysis of integer programs via triangular weakly non-linear loops ⋮ Runtime complexity analysis of logically constrained rewriting

Uses Software

• Aspic
• KITTeL

This page was built for publication: Termination Analysis of C Programs Using Compiler Intermediate Languages