An implementation of a verification condition generator for foundational proof-carrying code. - Jiangong Weng; Amy P. Felty (PST, 2011)