| ||||
| ||||
![]() Title:Procedure-Modular Termination Analysis Conference:WST 2018 Tags:bit precise, interprocedural analysis, interprocedural termination analysis, modular termination analysis, proving termination, termination, termination analysis and verification 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 focused 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. Procedure-Modular Termination Analysis ![]() Procedure-Modular Termination Analysis | ||||
Copyright © 2002 – 2025 EasyChair |