Modular verification

[Google Scholar]

Notes: loop invariant, contract driven development
Papers: calcagno:popl:2009


See also contract driven development. loop invariant

One of the big challenges in modular verification is the effort of creating contracts for every function in a large, existing codebase. One attack on that problem is biabduction calcagno:popl:2009.

Contract driven development, Spec# project