Case Based Specifications – reusing specifications, programs and proofs
Rosemary Monahan, Diarmuid O’Donoghue · Maynooth University ePrints and eTheses Archive (Maynooth University) · 2012
Many software verification tools use the design-by-contract approach to annotate programs with assertions so that tools, such as compilers, can generate the proof obligations required to verify that a program satisfies its specification. Theorem provers and SMT solvers are then used to, often automatically, discharge the proof obligations that have been generated.