Sorcar - Property-Driven Algorithms for Learning Conjunctive Invariants.

We present a new learning algorithm SORCAR to synthesize conjunctive inductive invariants for proving that a program satisfies its assertions. The salient property of this algorithm is that it is property-driven, and for a fixed finite set of n predicates, guarantees convergence in 2n rounds, taking only polynomial time in each round. We implement and evaluate the algorithm and show that its performance is favorable to the existing Houdini algorithm (which is not property-driven) for a class of benchmarks that prove data race freedom of GPU programs and another class that synthesizes invariants for proving separation logic properties for heap manipulating programs.