A specialization calculus for pruning disjunctive predicates to support verification

Wei Ngan Chin, Cristian Gherghina, Rǎzvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)
98 Downloads (Pure)


Separation logic-based abstraction mechanisms, enhanced with user-defined inductive predicates, represent a powerful, expressive means of specifying heap-based data structures with strong invariant properties. However, expressive power comes at a cost: the manipulation of such logics typically requires the unfolding of disjunctive predicates which may lead to expensive proof search. We address this problem by proposing a predicate specialization technique that allows efficient symbolic pruning of infeasible disjuncts inside each predicate instance. Our technique is presented as a calculus whose derivations preserve the satisfiability of formulas, while reducing the subsequent cost of their manipulation. Initial experimental results have confirmed significant speed gains from the deployment of predicate specialization. While specialization is a familiar technique for code optimization, its use in program verification is new.

Original languageEnglish
Title of host publicationComputer aided verification
Subtitle of host publicationLecture Notes in Computer Science
EditorsG Gopalakrishnan, S Qadeer
Place of PublicationBerlin
Number of pages17
ISBN (Print)9783642221095
Publication statusPublished - 20 Jul 2011
Event23rd International Conference on Computer Aided Verification - Snowbird, UT, United States
Duration: 14 Jul 201120 Jul 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6806 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International Conference on Computer Aided Verification
Abbreviated titleCAV 2011
Country/TerritoryUnited States
CitySnowbird, UT


Dive into the research topics of 'A specialization calculus for pruning disjunctive predicates to support verification'. Together they form a unique fingerprint.

Cite this