W.N. Chin
Verifying safety policies with size properties and alias controls
Chin, W.N.; Khoo, S.C.; Qin, S.; Popeea, C.; Nguyen, H.H.
Authors
S.C. Khoo
S. Qin
C. Popeea
H.H. Nguyen
Abstract
Many software properties can be analysed through a relational size analysis on each function’s inputs and outputs. Such relational analysis (through a form of dependent typing) has been successfully applied to declarative programs, and to restricted imperative programs; but it has been elusive for object-based programs. The main challenge is that objects may mutate and they may be aliased. In this paper, we show how safety policies of programs can be analysed by tracking size properties of objects and be enforced by objects’ invariants and the preconditions of methods. We propose several new ideas to allow both mutability and sharing of objects, whilst aiming for precision in our analysis. We introduce the concept of size-immutability to facilitate sharing, and also a set of alias controls to track unaliased objects whose size properties may change. We formalise our results through a set of advanced type checking rules for an object-based imperative language. We re-affirm the utility of the proposed type system by showing how a variety of software properties can be automatically verified according to size-inspired safety policies.
Citation
Chin, W., Khoo, S., Qin, S., Popeea, C., & Nguyen, H. (2005). Verifying safety policies with size properties and alias controls. In Proceedings of the 27th International Conference on Software Engineering, ICSE 05, 15-21 May 2005, St Louis MO (186-195). https://doi.org/10.1145/1062455.1062500
Conference Name | 27th International Conference on Software Engineering : ICSE'05. |
---|---|
Conference Location | St. Louis, Mo. |
Start Date | May 15, 2005 |
End Date | May 21, 2005 |
Publication Date | 2005-05 |
Deposit Date | Jan 23, 2009 |
Publisher | Association for Computing Machinery (ACM) |
Pages | 186-195 |
Book Title | Proceedings of the 27th International Conference on Software Engineering, ICSE 05, 15-21 May 2005, St Louis MO. |
DOI | https://doi.org/10.1145/1062455.1062500 |
Keywords | Object-based programs, Safety verification, Dependent types, Size properties, Alias control. |
Publisher URL | http://doi.acm.org/10.1145/1062455.1062500 |
You might also like
PTSC: probability, time and shared-variable concurrency
(2009)
Journal Article
Memory Usage Verification Using Hip/Sleek
(2009)
Conference Proceeding
An Interval-based Inference of Variant Parametric Types
(2009)
Conference Proceeding
A Heap Model for Java Bytecode to Support Separation Logic
(2008)
Conference Proceeding