Software inspections we can trust

Software is devilishly hard to inspect. Serious errors can escape attention for years. Consequently, many are hesitant to employ software in safety-critical applications and developers and users are finding the correction of software errors to be an increasingly burdensome cost. This talk describes a procedure for inspecting software that consistently finds subtle errors in software that is believed to be correct. The procedure is based on four key principles: * All reviewers actively use the code. * Reviewers exploit the hierarchical structure of the code rather than proceeding sequentially through the code. * Reviewers focus on small sections of code, producing precise summaries that are used when inspecting other sections. The summaries provide the links between the sections. * Reviewers proceed systematically so that no case, and no section of the program, gets overlooked. The inspectors produce and review mathematical documents. The mathematics allows them to check for complete coverage; tabular notation allows the work to proceed systematically in small steps.