Sciweavers

Share
ICSE
2005
IEEE-ACM

Verifying safety policies with size properties and alias controls

10 years 12 months ago
Verifying safety policies with size properties and alias controls
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 th...
Wei-Ngan Chin, Siau-Cheng Khoo, Shengchao Qin, Cor
Added 09 Dec 2009
Updated 09 Dec 2009
Type Conference
Year 2005
Where ICSE
Authors Wei-Ngan Chin, Siau-Cheng Khoo, Shengchao Qin, Corneliu Popeea, Huu Hai Nguyen
Comments (0)
books