We present a new modular shape analysis that can synthesize heap memory specification on a per method basis. We rely on a second-order biabduction mechanism that can give interpretations to unknown shape predicates. There are several novel features in our shape analysis. Firstly, it is grounded on second-order bi-abduction. Secondly, we distinguish unknown pre-predicates in pre-conditions, from unknown post-predicates in post-condition; since the former may be strengthened, while the latter may be weakened. Thirdly, we provide a new heap guard mechanism to support more precise preconditions for heap specification. Lastly, we formalise a set of derivation and normalization rules to give concise definitions for unknown predicates. Our approach has been proven sound and is implemented on top of an existing automated verification system.We show its versatility in synthesizing a wide range of intricate shape specifications. © 2014 Springer International Publishing.
CITATION STYLE
Le, Q. L., Gherghina, C., Qin, S., & Chin, W. N. (2014). Shape analysis via second-order bi-abduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8559 LNCS, pp. 52–68). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_4
Mendeley helps you to discover research relevant for your work.