Symbolic Execution for Sequential and Multi-Process Programs with Unbounded Loops

Symbolic execution is a powerful technique for automatically verifying properties of programs. Symbolic techniques have been developed for a variety of classes of assertions, to verify parallel as well as sequential programs, and even to verify functional equivalence of two programs. However, one limitation of these applications is that they typically require that constant (often small) bounds be imposed on the number of loop iterations. We present a generalization of symbolic execution that can reason about loops without bounds. This approach requires a user-provided loop invariant, but is otherwise fully automatic. Most importantly, it generalizes naturally to multi-process message-passing programs, and to verification of functional equivalence. We have realized the technique in the Toolkit for Accurate Scientific Software and demonstrated its effectiveness on several examples.