Bit-Precise Procedure-Modular Termination Analysis

Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter Wachter

Research output: Contribution to journalArticle (Academic Journal)peer-review

57 Downloads (Pure)

Abstract

Non-termination is the root cause of a variety of program bugs, such as hanging programs and denial-ofservice vulnerabilities. This makes an automated analysis that can prove the absence of such bugs highly desirable. To scale termination checks to large systems, an interprocedural termination analysis seems essential. This is a largely unexplored area of research in termination analysis, where most effort has focussed on small but difficult single-procedure problems. We present a modular termination analysis for C programs using template-based interprocedural summarisation. Our analysis combines a context-sensitive, over-approximating forward analysis with the inference of under-approximating preconditions for termination. Bit-precise termination arguments are synthesised over lexicographic linear ranking function templates. Our experimental results show the advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.
Original languageEnglish
Article number1
Number of pages38
JournalACM Transactions on Programming Languages and Systems
Volume40
Issue number1
DOIs
Publication statusPublished - 1 Dec 2017

Structured keywords

  • Programming Languages

Keywords

  • bit-precise analysis
  • interprocedural analysis
  • templates
  • Termination analysis

Cite this