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 |
Related
| Distinct from | garavel2020expert |
|---|---|
| Distinct from | kneuper1997limits |
| Distinct from | luqi1997formal |
| Distinct from | rushby1999partitioning |
| Distinct from | rushby2007automated |
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.
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.