Loop Invariant Symbolic Execution for Parallel Programs

Techniques for verifying program assertions using symbolic execution exhibit a significant limitation: they typically require that constant (often small) bounds be imposed on the number of loop iterations. For sequential programs, there is a way to overcome this limitation using loop invariants. The basic idea is to assign new symbolic constants to the variables modified in the loop body, add the invariant to the path condition, and then explore two paths: one which executes the loop body and checks that the given invariant is inductive, the other which jumps to the location just after the loop. For parallel programs, the situation is more complicated: the invariant may relate the state of multiple processes, these processes may enter and exit the loop at different times, and they may be at different iteration counts at the same time. In this paper, we show how to overcome these obstacles. Specifically, we introduce the notion of collective loop invariant and a symbolic execution technique that uses it to verify assertions in message-passing parallel programs with unbounded loops, generalizing the sequential technique.

@inproceedings{siegel-zirkel:2012:loops,
  Author = {Stephen F. Siegel and Timothy K. Zirkel},
  Crossref = {vmcai2012},
  Pages = {412--427},
  Title = {Loop Invariant Symbolic Execution for Parallel Program}}

@proceedings{vmcai2012,
  Booktitle = {Verification, Model Checking, and Abstract Interpretation: 13th International Conference, {VMCAI} 2012},
  Editor = {Kuncak, Viktor and Rybalchenko, Andrey},
  Publisher = {Springer},
  Series = {Lecture Notes in Computer Science},
  Title = {Verification, Model Checking, and Abstract Interpretation: 13th International Conference, {VMCAI} 2012, Philadelphia PA, USA, January 22--24, 2012, Proceedings},
  Volume = {7148},
  Year = 2012
}