Maximal and Compositional Pattern-Based Loop Invariants
Pierre Courtieu, Aponte, Maria-Virginia, Yannick Moy, Marc Sango · HAL (Le Centre pour la Communication Scientifique Directe) · 2012
We define a framework for automatic generation of loop invariants for a small language. The method proceeds by 1) translation to an intermediate language of parallel guarded assignments 2) pattern detection. The patterns are modular in the sense that they are independent of the loop they appear in. Some maximality results are also proved on some pattern invariants.