A Fixed-Point Algorithm for Automated Static Detection of Infinite Loops

We present an algorithm for automated detectionof infinite loop bugs in programs. It relies on a SatisfiabilityModulo Theories (SMT) solver backend and can be runconveniently with SMT-constrained symbolic execution. Thealgorithm detects infinite loop bugs for single-path, multi-pathand nested loops. We prove soundness of the algorithm, i.e.there are no false positive detections of infinite loops. Part of thealgorithm is a fixed-point based termination check for ’simple’loops, whose soundness is a consequence of Brouwer’s fixed-point theorem. The algorithm further yields no false negativedetections for context-sensitive detection of periodic loop orbitswith sum of prefix iterations and periodicity of up to theanalysis loop unroll depth (bounded completeness), if the SMTsolver answers the fixed-point satisfiability query in time. Wedescribe an example implementation as plug-in extension ofEclipse CDT. The implementation is validated with the infiniteloop test cases from the Juliet test suite and benchmarks areprovided.