University of Sussex
Browse
paper.pdf (514.18 kB)

Bit-precise procedure-modular termination analysis

Download (514.18 kB)
journal contribution
posted on 2023-06-09, 07:30 authored by Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter
Non-termination is the root cause of a variety of program bugs, such as hanging programs and denial-of-service 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.

History

Publication status

  • Published

File Version

  • Accepted version

Journal

ACM Transactions on Programming Languages and Systems

ISSN

0164-0925

Publisher

ACM Press

Issue

1

Volume

40

Page range

1-38

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2017-08-02

First Open Access (FOA) Date

2017-12-12

First Compliant Deposit (FCD) Date

2017-08-01

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC