Tool support for verification-based software inspection

For a software component to be reusable, it must be verified as correct and documented with an unambiguous and complete specification of what it does. We present a technique of semiformal verification using tool support. The prototype tool MINDER generates specifications and verification conditions directly from program code at the unit level. As opposed to systems involving theorem proving, this approach is directed at supporting human reasoning during verification-based software inspection. In effect MINDER provides guidance for inspectors constructing arguments of correctness. The output of MINDER is also useful for documenting a formal specification for a program. We demonstrate with simple examples the use of MINDER in supporting the verification and publication of trusted unit-level software components.