Output details
11 - Computer Science and Informatics
Teesside University
Enhancing modular OO verification with separation logic
<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.