Options
Can Computer Programs be Formally Verified?
Angius, Nicola
2023
Loading...
Abstract
Questo articolo esamina il problema, centrale in filosofia dell’informatica, inerente la possibilità di verificare i programmi per calcolatore mediante una dimostrazione matematica. In primo luogo, viene definita la verifica software e viene ricordato il dibattito classico sulla sua possibilità alla luce di una ontologia dualistica dei sistemi computazionali. In secondo luogo, viene analizzato il dibattito attuale sottolineando le motivazioni logiche, tecnologiche e filosofiche del suo rinnovato interesse. Infine, viene mostrato come, adottando un’ontologia stratificata per i sistemi computazionali, si possano ricombinare le diverse posizioni nel dibattito, sostenendo come la verifica software richieda tanto il ragionamento deduttivo quanto quello induttivo.
This paper examines one central problem in the philosophy of computer science, namely the question of whether computer programs can be verified by means of a mathematical proof. Firstly, program verification is defined and the classical debate on its feasibility is recalled under the light of a dual ontology of computational systems. Secondly, the current resurgence of the debate is analysed underlining its logical, technological, and philosophical motivations. Finally, it is shown how adopting a stratified ontology for computational systems one may recombine the different positions in the debate, arguing how program verification involves both deductive and inductive reasoning
Questo articolo esamina il problema, centrale in filosofia dell’informatica, inerente la possibilità di verificare i programmi per calcolatore mediante una dimostrazione matematica. In primo luogo, viene definita la verifica software e viene ricordato il dibattito classico sulla sua possibilità alla luce di una ontologia dualistica dei sistemi computazionali. In secondo luogo, viene analizzato il dibattito attuale sottolineando le motivazioni logiche, tecnologiche e filosofiche del suo rinnovato interesse. Infine, viene mostrato come, adottando un’ontologia stratificata per i sistemi computazionali, si possano ricombinare le diverse posizioni nel dibattito, sostenendo come la verifica software richieda tanto il ragionamento deduttivo quanto quello induttivo.
Journal
Source
Nicola Angius, "Can Computer Programs be Formally Verified?", in "APhEx 28", 2023, pp. 322-338
Languages
en
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International
File(s)
Loading...
Name
APhEx28, 2023CanComputerProgramsbeFormallyVerified.pdf
Format
Adobe PDF
Size
508.07 KB