Software Verification and System Assurance
The work
| Authors | John Rushby |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2009 |
| Citekey | rushby2009software |
Where it appeared
| Published in | 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods |
|---|---|
| Publisher | IEEE |
| Pages | 3--10 |
Identifiers
| DOI | 10.1109/sefm.2009.39 |
|---|
Access
| URL | https://www.csl.sri.com/users/rushby/papers/sefm09.pdf |
|---|---|
| Landing page | https://doi.org/10.1109/sefm.2009.39 |
Abstract
Littlewood [1] 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.
A copy is held
pdf, 82.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via unpaywall |
|---|---|
| Added | 2026-08-07 00:00 UTC |
| Approved by | a person 2026-08-14 11:33 UTC |
Filed under
do-formal-methods-pay drheap rushby sefm when-software-kills
Cite it as
@inproceedings{rushby2009software,
title = {Software Verification and System Assurance},
author = {John Rushby},
year = {2009},
booktitle = {2009 Seventh IEEE International Conference on Software Engineering and Formal Methods},
publisher = {IEEE},
pages = {3--10},
doi = {10.1109/sefm.2009.39},
}
This record lives at https://refs.drheap.org/rushby2009software/ and will keep doing so.