Trace Compression with Loop Explanations

We present a method of compressing long traces by discovering invariants for loops it has iterated through. The invariants discov-ered are such that the resulting compressed trace also satisfies cer-tain “target properties ” which the original trace satisfied (say, an assertion at the end). This results in a concise trace that explains why the original trace satisfied the target without needing to unroll the loops fully. A central feature is the use of a canonical loop in-variant discovery algorithm which preserves all atomic formulas in the representation of a symbolic state which can be shown to be invariant. If this fails to provide a “safe ” invariant, then the algo-rithm dynamically unrolls the loop and attempts the discovery at the next iteration, where it is more likely to succeed as the loop stabilizes towards an invariant. We show via realistic benchmarks, which present the compressed trace as a Hoare proof, that the end result is signicantly more succinct than the original trace. 1