Please use this identifier to cite or link to this item: https://doi.org/10.1145/1328438.1328452
DC FieldValue
dc.titleEnhancing modular OO verification with separation logic
dc.contributor.authorChin, W.-N.
dc.contributor.authorDavid, C.
dc.contributor.authorNguyen, H.H.
dc.contributor.authorQin, S.
dc.date.accessioned2013-07-04T07:56:43Z
dc.date.available2013-07-04T07:56:43Z
dc.date.issued2008
dc.identifier.citationChin, 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. https://doi.org/10.1145/1328438.1328452
dc.identifier.isbn9781595936899
dc.identifier.issn07308566
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/40103
dc.description.abstractConventional 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.
dc.description.urihttp://libproxy1.nus.edu.sg/login?url=http://dx.doi.org/10.1145/1328438.1328452
dc.sourceScopus
dc.subjectautomated verification
dc.subjectenhanced subsumption
dc.subjectlossless casting
dc.subjectseparation logic
dc.subjectstatic and dynamic specifications
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.doi10.1145/1328438.1328452
dc.description.sourcetitleConference Record of the Annual ACM Symposium on Principles of Programming Languages
dc.description.page87-99
dc.description.codenCRLAD
dc.identifier.isiut000265876500009
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

28
checked on Aug 12, 2022

WEB OF SCIENCETM
Citations

17
checked on Aug 12, 2022

Page view(s)

142
checked on Aug 4, 2022

Google ScholarTM

Check

Altmetric


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