todo

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.

Notes related to Modular verification

Contract driven development, Spec# project

Papers related to Modular verification

• Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
• Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
• Verification of concurrent programs with Chalice [leino:fosad:2007]
• No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]