Loop Refinement Using Octagons and Satisfiability.

This paper presents a technique for refining the control structure of loops in programs operating over finite bit-vectors. 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.