Towards feasible, machine-assisted verification of object-oriented programs. - Francis Hin-Lun Tang (2002)