Resource protocol verification for OO programs

The first contribution of this project was a dependent type system for verifying resource protocols for first-order functional programs [1]. We extended the type system with support for aliasing information and applied it for verifying object-oriented programs. For example, our type system guarantees safety of a bounded buffer resource that neither underflows or overflows based on the interface property of a wrap-around (or cyclic) array.

  1. PEPM 2004 A Type System for Resource Protocol Verification and its Correctness Proof (pdf)
  2. ICSE 2005 Verifying Safety Policies with Size Properties and Alias Controls (pdf) (slides)

This project has been carried at the National University of Singapore and is joint work with my PhD advisor, Wei-Ngan Chin. The paper [1] is co-authored with Siau-Cheng Khoo, Huu Hai Nguyen and Shengchao Qin.