Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
sav08:exercises_05 [2008/03/18 18:35] vkuncak |
sav08:exercises_05 [2008/03/25 14:02] piskac |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Exercises 05 ====== | ====== Exercises 05 ====== | ||
+ | |||
+ | * Talk by Wei Ngan Chin: "Enhancing Modular OO Verification via Separation Logic" | ||
+ | |||
+ | |||
+ | 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. | ||
+ | |||
+ | |||
+ | |||
* Homework analysis | * Homework analysis |