Efficient Tight Field Bounds Computation Based on Shape Predicates

PONZIO, PABLO; ROSNER, NICOLÁS; AGUIRRE, NAZARENO; FRIAS, MARCELO

Conferencia; 19th International Symposium on Formal Methods; 2014

Formal Methods Europe

Tight field bounds contribute to verifying the correctness of object oriented programs in bounded scenarios, by restricting the values that fields can take to feasible cases only, during automated analysis. Tight field bounds are computed from formal class specifications. Their computation is costly, and existing approaches use a cluster of computers to obtain the bounds, from declarative (JML) formal specifications.In this article we address the question of whether the language in which class specifications are expressed may a↵ect the e ciency with which tight field bounds can be computed. We introduce a novel technique that generates tight field bounds from data structure descriptions provided in terms of shape predicates, expressed using separation logic. Our tech- nique enables us to compute tight field bounds faster on a single work- station, than the alternative approaches which use a cluster, in wall-clock time terms. Although the computed tight bounds di↵er in the canonical ordering in which data structure nodes are labeled, our computed tight field bounds are also e↵ective. We incorporate the field bounds computed with our technique into a state-of-the-art SAT based analysis tool, and show that, for various case studies, our field bounds allow us to handle scopes in bounded exhaustive analysis comparable to those correspond- ing to bounds computed with previous techniques.