### Compositional Shape Analysis by Means of Bi-AbductionCompositional Shape Analysis by Means of Bi-Abduction

Access Restriction
Subscribed

 Author Calcagno, Cristiano ♦ Distefano, Dino ♦ O'Hearn, Peter W. ♦ Yang, Hongseok Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2011 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword Abstract interpretation ♦ Compositionality ♦ Program proving ♦ Separation logic ♦ Static analysis Abstract The accurate and efficient treatment of mutable data structures is one of the outstanding problem areas in automatic program verification and analysis. Shape analysis is a form of program analysis that attempts to infer descriptions of the data structures in a program, and to prove that these structures are not misused or corrupted. It is one of the more challenging and expensive forms of program analysis, due to the complexity of aliasing and the need to look arbitrarily deeply into the program heap. This article describes a method of boosting shape analyses by defining a compositional method, where each procedure is analyzed independently of its callers. The analysis algorithm uses a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Our method brings the usual benefits of compositionality---increased potential to scale, ability to deal with incomplete programs, graceful way to deal with imprecision---to shape analysis, for the first time. The analysis rests on a generalized form of abduction (inference of explanatory hypotheses), which we call $\textit{bi-abduction}.$ Bi-abduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new analysis algorithm. We have implemented our analysis and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger code bases (e.g., sendmail, an imap server, a Linux distribution) to illustrate the level of automation and scalability that we obtain from our compositional method. This article makes number of specific technical contributions on proof procedures and analysis algorithms, but in a sense its more important contribution is holistic: the explanation and demonstration of how a massive increase in automation is possible using abductive inference. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2011-12-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 58 Issue Number 6 Page Count 66 Starting Page 1 Ending Page 66

#### Open content in new tab

Source: ACM Digital Library