Verification condition (VC) generation is a fundamental part of many program analysis and applications, including proving program correctness, automatic test case generation, proof carrying code, and others. In all application domains, there are two critical factors for VC generation algorithms: compact final VCs and fast VC generation. Compact VCs save more than bits; empirically compact formulas are easier to reason about in subsequent steps such as VC verification.
The theoretically most efficient algorithms for generating VCs are based upon weakest preconditions (WP). Current WP algorithms iterate over program statements backwards from the last statement in the program to the first, and can generate a VC that is at most O(M2) the size of a program. In practice, however, application domains that rely on VC generation often opt to use forward symbolic execution (FSE), which works in the forward direction from the first program statement to the last. Forward-based algorithms are attractive in practice because they easily afford optimizations such as eliminating constant expressions from VCs during generation. FSE, however, is theoretically exponentially worse than WP-based algorithms — it produces a separate VC for each program path, thus the final VC for all paths is O(2M).
We propose a new directionless weakest precondition that can be run in both the forward and backward direction. Our algorithm provides a O(M2) VC generation time and predicate size while affording optimizations that make FSE attractive in practice. We provide end-to-end proofs of correctness, size, and generation time. We then show how our approach leads to a proof of equivalence between VCs generated with WPs and FSE for typical structured programs.
A Technical Report on our Efficient DWP algorithm is available as CMU-Cylab-10-002.
We have implemented our DWP algorithm in BAP. There is work in progress to implement it in KLEE.
- Ivan Jager
- David Brumley