Compositional Shape Analysis by Means of Bi-Abduction

摘要: The accurate and efficient treatment of mutable data structures is one the outstanding problem areas in automatic program verification analysis. Shape analysis a form that attempts to infer descriptions program, prove these are not misused or corrupted. It more challenging expensive forms analysis, due complexity aliasing need look arbitrarily deeply into heap. This article describes method boosting shape analyses by defining compositional method, where each procedure analyzed independently its callers. algorithm uses restricted fragment separation logic, assigns collection Hoare triples procedure; provide an over-approximation structure usage. Our brings usual benefits compositionality---increased potential scale, ability deal with incomplete programs, graceful way imprecision---to for first time.The rests on generalized abduction (inference explanatory hypotheses), which we call bi-abduction. Bi-abduction displays as kind inverse frame problem: it jointly infers anti-frames (missing portions state) frames (portions state touched operation), basis new algorithm. We have implemented our report case studies smaller programs evaluate quality discovered specifications, larger code bases (e.g., sendmail, imap server, Linux distribution) illustrate level automation scalability obtain from method.This makes number specific technical contributions proof procedures algorithms, but sense important contribution holistic: explanation demonstration how massive increase possible using abductive inference.