Output details

A specialization calculus for pruning disjunctive predicates to support verification

<07> Separation-logic-based abstraction mechanisms, enhanced with user-defined inductive-predicates, represent a powerful, expressive means of specifying heap-based data structures with strong invariants. But it typically requires the unfolding of disjunctive-predicates leading to expensive proof search. We propose a predicate specialization technique allowing efficient symbolic pruning of infeasible disjuncts inside each predicate instance. Our technique is original as the derivations preserve the satisfiability of formulas, while reducing the subsequent cost of manipulation. It is novel as no one has proposed it for program verification before. The significance of the work is further confirmed by initial experimental results, demonstrating significant speed gains during verification.