Paper Info
Title
Bit-Precise Procedure-Modular Termination Analysis.
Abstract
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.
Year
Venue
Keywords
2018
ACM Trans. Program. Lang. Syst.
Termination analysis, bit-precise analysis, interprocedural analysis, templates
Field
DocType
Volume
Programming language,Ranking,Inference,Computer science,Theoretical computer science,Termination analysis,Modular design,Template,Lexicographical order,Root cause
Journal
40
Issue
Citations 
PageRank 
1
0
0.34
References 
Authors
54
5
Name
Order
Citations
PageRank
Hongyi Chen19510.61
Cristina David221.05
Daniel Kroening33084187.60
Peter Schrammel413419.10
Björn Wachter532620.09