Repository logo
 

Bit-precise procedure-modular termination analysis

Accepted version
Peer-reviewed

Type

Article

Change log

Authors

Chen, HY 
David, C 
Kroening, D 
Schrammel, P 
Wachter, B 

Abstract

jats:pNon-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.</jats:p> jats:pWe 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.</jats:p>

Description

Keywords

46 Information and Computing Sciences, 4602 Artificial Intelligence

Journal Title

ACM Transactions on Programming Languages and Systems

Conference Name

Journal ISSN

0164-0925
1558-4593

Volume Title

40

Publisher

Association for Computing Machinery (ACM)

Rights

All rights reserved