2004 Australian Software Engineering Conference (ASWEC'04)
Tool Support for Verification-Based Software Inspection
Melbourne, Australia
April 13-April 16
ISBN: 0-7695-2089-8
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. In this paper we present a technique of semi-formal verification using tool support. The prototype tool MINDER generates specifications and verification conditions directly from programcode 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. In this paper we demonstrate with simple examples the use of MINDER in supporting the verification and publication of trusted unit-level software components.