Modular verification of higher-order methods with mandatory calls specified by model programs.

Steve M. Shaner, Gary T. Leavens, David A. Naumann

Browse the full OOPSLA paper archive.