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.
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.