Paper Info
Title
Efficient Tight Field Bounds Computation Based on Shape Predicates.
Abstract
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 affect the efficiency 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 technique enables us to compute tight field bounds faster on a single workstation, than the alternative approaches which use a cluster, in wall-clock time terms. Although the computed tight bounds differ in the canonical ordering in which data structure nodes are labeled, our computed tight field bounds are also effective. 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 corresponding to bounds computed with previous techniques.
Year
DOI
Venue
2014
10.1007/978-3-319-06410-9_36
Lecture Notes in Computer Science
Field
DocType
Volume
Data structure,Separation logic,Computer science,Correctness,Algorithm,Formal specification,Theoretical computer science,Bounds checking,Bounded function,Computation,Class invariant
Conference
8442
ISSN
Citations 
PageRank 
0302-9743
2
0.36
References 
Authors
20
4
Name
Order
Citations
PageRank
Pablo Ponzio1144.92
Nicolás Rosner2685.14
Nazareno Aguirre315921.79
Marcelo F. Frias429535.57