A FixedPoint 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 SMTconstrained symbolic execution. Thealgorithm detects infinite loop bugs for singlepath, multipathand nested loops. We prove soundness of the algorithm, i.e.there are no false positive detections of infinite loops. Part of thealgorithm is a fixedpoint based termination check for ’simple’loops, whose soundness is a consequence of Brouwer’s fixedpoint theorem. The algorithm further yields no false negativedetections for contextsensitive 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 fixedpoint satisfiability query in time. Wedescribe an example implementation as plugin extension ofEclipse CDT. The implementation is validated with the infiniteloop test cases from the Juliet test suite and benchmarks areprovided.
A FixedPoint Algorithm for Automated Static Detection of Infinite Loops
IEEE Int. Symp. High Assurance Systems Eng.
Authors:  Andreas Ibing and A. Mai 
Year/month:  2015/1 
Booktitle:  IEEE Int. Symp. High Assurance Systems Eng. 
Fulltext:  ibing15infloops.pdf 
Abstract 

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 SMTconstrained symbolic execution. Thealgorithm detects infinite loop bugs for singlepath, multipathand nested loops. We prove soundness of the algorithm, i.e.there are no false positive detections of infinite loops. Part of thealgorithm is a fixedpoint based termination check for ’simple’loops, whose soundness is a consequence of Brouwer’s fixedpoint theorem. The algorithm further yields no false negativedetections for contextsensitive 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 fixedpoint satisfiability query in time. Wedescribe an example implementation as plugin extension ofEclipse CDT. The implementation is validated with the infiniteloop test cases from the Juliet test suite and benchmarks areprovided. 
Bibtex:
@inproceedings {author = { Andreas Ibing and A. Mai},
title = { A FixedPoint Algorithm for Automated Static Detection of Infinite Loops },
year = { 2015 },
month = { January },
booktitle = { IEEE Int. Symp. High Assurance Systems Eng. },
url = {https://www.sec.in.tum.de/i20/publications/afixedpointalgorithmforautomatedstaticdetectionofinfiniteloops/@@download/file/ibing15infloops.pdf}
}