Loop Refinement Using Octagons and Satisfiability
This paper presents a technique for refining the control structure of loops in programs operating over finite bitvectors. This technique is based on abstract interpretation using octagons and affine equalities in order to identify infeasible sequences of loop iterations. Our approach naturally integrates wrap-around arithmetic during the generation of abstractions. Abstract interpreters operating on a refined control structure then typically derive strengthened program invariants without having to rely on complicated domain constructions such as disjunctive completions.
Jörg Brauer, Volker Kamin, Stefan Kowalewski and Thomas Noll