• 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