Why There is no General Solution to the Problem of Software Verification

&
Foundations of Science 25 (3):541-557 (2020)
  Copy   BIBTEX

Abstract

How can we be certain that software is reliable? Is there any method that can verify the correctness of software for all cases of interest? Computer scientists and software engineers have informally assumed that there is no fully general solution to the verification problem. In this paper, we survey approaches to the problem of software verification and offer a new proof for why there can be no general solution.

Categories

Keywords

Reprint years

DOI

10.1007/s10699-019-09611-w

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 94,045

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Why There is no General Solution to the Problem of Software Verification.John Symons & Jack J. Horner - 2020 - Foundations of Science 25 (3):541-557.
Computational Idealizations in Software Intensive Science: a Comment on Symons’ and Horner’s paper.Nicola Angius - 2014 - Philosophy and Technology 27 (3):479-484.
A Dynamic Software Certification and Verification Procedure.Julio Michael Stern & Carlos Alberto de Braganca Pereira - 1998 - SCI’99 Proceedings 2:426-435.
Problems for a Philosophy of Software Engineering.Stefan Gruner - 2011 - Minds and Machines 21 (2):275-299.
Halting problem proofs refuted on the basis of software engineering ?P. Olcott - manuscript
The Matrix-Graph Method Of Choice And Verification Of Software Reliability Models.V. S. Kharchenko, O. M. Tarasyuk & V. V. Sklyar - forthcoming - Philosophy of Science.
Kant and the software crisis: Suggestions for the construction of human-centred software systems. [REVIEW]Marco C. Bettoni - 1995 - AI and Society 9 (4):396-401.
Towards a Philosophy of Software Development: 40 Years after the Birth of Software Engineering.Mandy Northover, Derrick G. Kourie, Andrew Boake, Stefan Gruner & Alan Northover - 2008 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 39 (1):85-113.
Why Separation Logic Works.David Pym, Jonathan M. Spring & Peter O’Hearn - 2019 - Philosophy and Technology 32 (3):483-516.
Halting problem undecidability and infinitely nested simulation (V5).P. Olcott - manuscript

Analytics

Added to PP
2019-06-03

Downloads
18 (#828,658)

6 months
5 (#837,836)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

John Symons
University of Kansas

Citations of this work

Software engineering standards for epidemiological models.Jack K. Horner & John F. Symons - 2020 - History and Philosophy of the Life Sciences 42 (4):1-24.

Add more citations

References found in this work

Computing machinery and intelligence.Alan M. Turing - 1950 - Mind 59 (October):433-60.
On Computable Numbers, with an Application to the Entscheidungsproblem.Alan Turing - 1936 - Proceedings of the London Mathematical Society 42 (1):230-265.
In defense of proper functions.Ruth Millikan - 1989 - Philosophy of Science 56 (June):288-302.
Computing Machinery and Intelligence.Alan M. Turing - 2003 - In John Heil (ed.), Philosophy of Mind: A Guide and Anthology. New York: Oxford University Press.
Model Theory.Michael Makkai, C. C. Chang & H. J. Keisler - 1991 - Journal of Symbolic Logic 56 (3):1096.

View all 20 references / Add more references