Software Verification and System Assurance

John Rushby

Invited paper, presented at the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM), Hanoi, Vietnam, November 2009. Appears in the proceedings, pp. 1--9, © IEEE Computer Society

Abstract

Littlewood [IEEE TSE 200] 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.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

Slides

PDF or crude ascii (for your Palm Pilot)

BibTeX Entry


@INPROCEEDINGS{Rushby09:SEFM,
	AUTHOR = {John Rushby},
	TITLE = {Software Verification and System Assurance},
	BOOKTITLE = {Seventh International Conference on Software Engineering and Formal Methods ({SEFM})},
	EDITOR = {Dang Van Hung and Padmanabhan Krishnan},
	ADDRESS = {Hanoi, Vietnam},
	ORGANIZATION = {IEEE Computer Society},
	PAGES = {3--10},
	MONTH = nov,
	YEAR = 2009
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page