Bit-precise procedure-modular termination analysis
ACM Transactions on Programming Languages and Systems
MetadataShow full item record
Chen, H., David, C., Kroening, D., Schrammel, P., & Wachter, B. (2017). Bit-precise procedure-modular termination analysis. ACM Transactions on Programming Languages and Systems, 40 (1)https://doi.org/10.1145/3121136
© 2017 Copyright is held by the owner/author(s). 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 summari-sation. 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.
External DOI: https://doi.org/10.1145/3121136
This record's URL: https://www.repository.cam.ac.uk/handle/1810/294332
All rights reserved