Sometimes some loops do not terminate. That is, the program sticks in the loop, iterating infinitely often because of an error. We addressed this problem in the new version of Loopfrog 0.9, which features termination analysis support and is able to discover non-terminating loops.
For that, we added a library of abstract domains to discover well-founded transition invariants, necessary to infer termination of the loop. This way, in contrast to other methods like Terminator or Compositional Termination Analysis [1], it aims to construct a complete ranking argument for all paths in a loop at once, thus, avoiding expensive enumeration of individual paths. Compositionality is used as a criterion of completeness for discovered transition invariants.
The practical efficiency of the approach is demonstrated on a set of Windows device drivers. Preliminary results of experiments on loop summarization with termination:
The models for experiments are extracted using goto-cc tool (version 3.3). Pre-compiled models for several benchmarks, in particular, Windows Device Drivers, are available in cprover.org collection.
References
- Termination Analysis with Compositional Transition Invariants, , International Conference on Computer-Aided Verification (CAV), Edinburgh, UK, p.89-103, Springer (2010)
