Differences

This shows you the differences between two versions of the page.

--- sav08:exercises_05 [2008/03/18 18:35]
vkuncak
+++ sav08:exercises_05 [2008/03/25 14:02]
piskac
@@ Line 1: / Line 1: @@
 ====== 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
   * Semantic proof of drinker's paradox
-  * Monotonicity of semantic consequence
-  * Sets of sentences with only finite and with only infinite models
-  * Herbrand universe
-  * Resolution proofs