Please use this identifier to cite or link to this item:
Title: Enhancing modular OO verification with separation logic
Authors: Chin, W.-N. 
David, C.
Nguyen, H.H. 
Qin, S.
Keywords: automated verification
enhanced subsumption
lossless casting
separation logic
static and dynamic specifications
Issue Date: 2008
Citation: Chin, W.-N., David, C., Nguyen, H.H., Qin, S. (2008). Enhancing modular OO verification with separation logic. Conference Record of the Annual ACM Symposium on Principles of Programming Languages : 87-99. ScholarBank@NUS Repository.
Abstract: Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this. © 2008 ACM.
Source Title: Conference Record of the Annual ACM Symposium on Principles of Programming Languages
ISBN: 9781595936899
ISSN: 07308566
DOI: 10.1145/1328438.1328452
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Sep 21, 2022


checked on Sep 21, 2022

Page view(s)

checked on Sep 22, 2022

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.