A Theoretical Study of the Synergy and Lazy Annotation Algorithms

Abstract

Given a program with assertions, the assertion checking problem is to tell whether there is an execution of the program that violates one of the assertions. One approach to this problem is to explore different paths towards assertion violations, and to learn “blocking” conditions whenever a path is blocked from reaching the violations. The Synergy algorithm of Gulavani et al. [FSE 2006] and the Lazy Annotation algorithm of McMillan [CAV2010] are two recent algorithms that follow this approach to assertion checking. Each technique has its own advantages. Synergy uses concrete tests which are very cheap as compared to theorem prover calls. The tests also help by giving us the place to perform the refinement (called the frontier) for an abstraction which is too coarse. Synergy uses partition refinement while maintaining its abstraction. The Lazy Annotation algorithm basically partitions each location in to regions that are safe and unsafe. The safe regions are those from which we cannot reach the error states, and the unsafe regions are the remaining ones. The annotations that this algorithm maintains correspond to the safe regions. The advantage that annotations have over partition refinement is that annotations can recover from irrelevant predicates used for annotating, where as once a partition is refined with an irrelevant predicate, it cannot recover from it. In this work, we make a theoretical study of the algorithms mentioned above. The aim of the study is to answer questions like: Is one algorithm provably better than the other, in terms of the best-case execution (counting the number of refinement steps) on input programs? Is the termination behavior of one always better than the other? We show that the Synergy and Lazy Annotation algorithms are incomparable, i.e., neither of them is provably better than the other, in terms of their best-case execution times. We also show how we can view the two algorithms on a common ground, in the sense that we show how to translate a snapshot of one algorithm into a snapshot of the other. This allows us to import the heuristics of one algorithm into the other, and there by propose new and potentially improved versions of these algorithms. By viewing them o n a common ground, we are also able to view the final proofs generated by the algorithms in either representation. We go on to study the proposed new versions of the Synergy and Lazy Annotation, comparing their best-case running times and their termination behaviour. We show that the following pairs of algorithms are incomparable: Mod-Syn (Lazy Annotation-style refinement imported into Synergy) and Synergy, Mod-Syn and Lazy Annotation, Synergy and SEAL(Synergy heuristics imported into Lazy Annotation). We show that the SEAL algorithm always performs better than the Lazy Annotation algorithm.