J. Rushby, “Software Verification and System Assurance,” 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009, pp. 3-10, doi: 10.1109/SEFM.2009.39.
Abstract
Littlewood introduced the idea that software may be possibly perfect and that we can contemplate its probability of (im)perfection. We review this idea and show how it provides a bridge between correctness, which is the goal of software verification (and especially formal verification), and the probabilistic properties such as reliability that are the targets for system-level assurance. We enumerate the hazards to formal verification, consider how each of these may be countered, and propose relative weightings that an assessor may employ in assigning a probability of perfection.
Keywords: Software systems, Formal verification, Software safety, Hazards, Failure analysis, Software engineering, Computer science, Laboratories