Output details
11 - Computer Science and Informatics
Teesside University
Output title
Enhancing modular OO verification with separation logic
Type
E - Conference contribution
Name of conference/published proceedings
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Volume number
-
Issue number
-
First page of article
87
ISSN of proceedings
-
Year of publication
2008
Number of additional authors
3
Additional information
<07> We present an enhanced approach to modular verification of object-oriented programs, based on the co-existence of both static and dynamic specifications, together with a principle that each static specification be a subtype of its corresponding dynamic specification. In addition to the distinction of static and dynamic specifications, we also formulate a novel specification subsumption that can avoid code re-verification. Our work is original as no one else has similar proposals (a similar proposal is reported at the same time and appears in the same proceedings). It is significant as it lays down a foundation for practical OO verification.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
3
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
