W.-N. Chin
Enhancing Modular OO Verification with Separation Logic
Chin, W.-N.; David, C.; Nguyen, H.H.; Qin, S.; Necula, G.C.; Wadler, P.
Authors
C. David
H.H. Nguyen
S. Qin
G.C. Necula
P. Wadler
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.
Citation
Chin, W., David, C., Nguyen, H., Qin, S., Necula, G., & Wadler, P. (2008). Enhancing Modular OO Verification with Separation Logic. In 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 7-12 January, 2008, San Francisco, California, USA ; proceedings (87-99). https://doi.org/10.1145/1328897.1328452
Conference Name | The 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008) |
---|---|
Conference Location | San Francisco, USA |
Start Date | Jan 10, 2008 |
End Date | Jan 12, 2008 |
Publication Date | Jan 1, 2008 |
Deposit Date | Nov 16, 2009 |
Volume | 43 |
Pages | 87-99 |
Series Title | ACM conference proceedings. |
Series Number | 1 |
Series ISSN | 0362-1340 |
Book Title | 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 7-12 January, 2008, San Francisco, California, USA ; proceedings. |
DOI | https://doi.org/10.1145/1328897.1328452 |
Keywords | Automated verification, Enhanced subsumption, Separation. |
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
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search