Diagnosing Abstraction Failure for Separation Logic--based Analyses

Diagnosing Abstraction Failure for Separation Logic--based Analyses,Josh Berdine,Arlen Cox,Samin Ishtiaq,Christoph M. Wintersteiger

Diagnosing Abstraction Failure for Separation Logic--based Analyses  
BibTex | RIS | RefWorks Download
Abstraction renement is an eective verication technique for automatically proving safety properties of software. Application of this technique in shape analyses has proved impractical as core compo- nents of existing renement techniques such as backward analysis, gen- eral conjunction, and identication of unreachable but doomed states are computationally infeasible in such domains. We propose a new method to diagnose proof failures to be used in a renement scheme for Separation Logic{based shape analyses. To check feasibility of abstract error traces, we perform Bounded Model Check- ing over the traces using a novel encoding into SMT. A subsequent di- agnosis nds discontinuities on infeasible traces, and identies doomed states admitted by the abstraction. To construct doomed states, we give a model-nding algorithm for \symbolic heap" Separation Logic formulas, employing the execution machinery of the feasibility checker to search for concrete counter-examples. The diagnosis has been implemented in SLAyer, and we present a simple scheme for rening the abstraction of hierarchical data structures, and illustrate its eectiveness on bench- marks from the SLAyer test suite.
Published in 2012.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.