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.

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.

Various errors can affect scientific code and detecting them is a central concern within computational science. Could formal verification methods, which are now available tools, be widely adopted to guarantee the general reliability of scientific code? After discussing their benefits and drawbacks, we claim that, absent significant changes as regards features like their user-friendliness and versatility, these methods are unlikely to be adopted throughout computational science, beyond certain specific contexts for which they are well-suited. This issue exemplifies the epistemological (...) heterogeneity of computational science: profoundly different practices can be appropriate to meet the reliability challenge that rises for scientific code. (shrink)

Various errors can affect scientific code and detecting them is a central concern within computational science. Could formal verification methods, which are now available tools, be widely adopted to guarantee the general reliability of scientific code? After discussing their benefits and drawbacks, we claim that, absent significant changes as regards features like their user-friendliness and versatility, these methods are unlikely to be adopted throughout computational science, beyond certain specific contexts for which they are well-suited. This issue exemplifies the epistemological (...) heterogeneity of computational science: profoundly different practices can be appropriate to meet the reliability challenge that rises for scientific code. (shrink)

The issue of proper functioning of operative computing and the utility of program verification, both in general and of specific methods, has been discussed a lot. In many of those discussions, attempts have been made to take mathematics as a model of knowledge and certitude achieving, and accordingly infer about the suitable ways to handle computing. I shortly review three approaches to the subject, and then take a stance by considering social factors which affect the epistemic status of both (...) mathematics and computing. I use the analogy between mathematics and computing in reverse—that is to say, I consider operative computing as a form of making mathematics, and so attempt to learn from computing to mathematics in general. I conclude that mathematics engineering is a field to be both developed for practical improvement of doing mathematics and taken into consideration while philosophizing about mathematics as well. (shrink)

Questions concerning the epistemological status of computer science are, in this paper, answered from the point of view of the formal verification framework. State space reduction techniques adopted to simplify computational models in model checking are analysed in terms of Aristotelian abstractions and Galilean idealizations characterizing the inquiry of empirical systems. Methodological considerations drawn here are employed to argue in favour of the scientific understanding of computer science as a discipline. Specifically, reduced models gained by Dataion are (...) acknowledged as Aristotelian abstractions that include only data which are sufficient to examine the interested executions. The present study highlights how the need to maximize incompatible properties is at the basis of both Abstraction Refinement, the process of generating a cascade of computational models to achieve a balance between simplicity and informativeness, and the Multiple Model Idealization approach in biology. Finally, fairness constraints, imposed to computational models to allow fair behaviours only, are defined as ceteris paribus conditions under which temporal formulas, formalizing software requirements, acquire the status of law-like statements about the software systems executions. (shrink)

A proof of ‘correctness’ for a mathematical algorithm cannot be relevant to executions of a program based on that algorithm because both the algorithm and the proof are based on assumptions that do not hold for computations carried out by real-world computers. Thus, proving the ‘correctness’ of an algorithm cannot establish the trustworthiness of programs based on that algorithm. Despite the (deceptive) sameness of the notations used to represent them, the transformation of an algorithm into an executable program is a (...) wrenching metamorphosis that changes a mathematical abstraction into a prescription for concrete actions to be taken by real computers. Therefore, it is verification of program executions (processes) that is needed, not of program texts that are merely the scripts for those processes. In this view, verification is the empirical investigation of: (a) the behavior that programs invoke in a computer system and (b) the larger context in which that behavior occurs. Here, deduction can play no more, and no less, a role than it does in the empirical sciences. (shrink)

A debate over the theoretical capabilities of formal methods in computer science has raged for more than two years now. The function of this paper is to summarize the key elements of this debate and to respond to important criticisms others have advanced by placing these issues within a broader context of philosophical considerations about the nature of hardware and of software and about the kinds of knowledge that we have the capacity to acquire concerning their performance.

This paper is concerned with the construction of theories of software systems yielding adequate predictions of their target systems’ computations. It is first argued that mathematical theories of programs are not able to provide predictions that are consistent with observed executions. Empirical theories of software systems are here introduced semantically, in terms of a hierarchy of computational models that are supplied by formal methods and testing techniques in computer science. Both deductive top-down and inductive bottom-up approaches in (...) the discovery of semantic software theories are refused to argue in favour of the abductive process of hypothesising and refining models at each level in the hierarchy, until they become satisfactorily predictive. Empirical theories of computational systems are required to be modular, as modular are most software verification and testing activities. We argue that logic relations must be thereby defined among models representing different modules in a semantic theory of a modular software system. We exclude that scientific structuralism is able to define module relations needed in software modular theories. The algebraic Theory of Institutions is finally introduced to specify the logic structure of modular semantic theories of computational systems. (shrink)

Since its conception nearly 20 years ago, Logic Programming - the idea of using logic as a programming language - has been developed to the point where it now plays an important role in areas such as database theory, artificial intelligence and software engineering. However, there are still many challenging research issues to be addressed and the UK branch of the Association for Logic Programming was set up to provide a forum where the flourishing research community could discuss important (...) issues of Logic Programming which were often by-passed at the large international conferences. This volume contains the twelve papers which were presented at the ALPUK's 3rd conference which was held in Edinburgh, 10-12 April 1991. The aim of the conference was to give a broad but detailed technical insight into the work currently being done in this field, both in the UK and by researchers as far afield as Canada and Bulgaria. The breadth of interest in this area of Computer Science is reflected in the range of the papers which cover - amongst other areas - massively parallel implementation, constraint logic programming, circuit modelling, algebraic proof of program properties, deductive databases, specialised editors and standardisation. The resulting volume gives a good overview of the current progress being made in the field and will be of interest to researchers and students of any aspects of logic programming, parallel computing or database techniques and management. (shrink)

Introduction -- Algorithms, programs, procedures, and abstract automata -- Functioning of algorithms and automata, computation, and operations with algorithms and automata -- Basic postulates and axioms for algorithms -- Power of algorithms and classes of algorithms: comparison and evaluation -- Computing, accepting, and deciding modes of algorithms and programs -- Problems that people solve and related properties of algorithms -- Boundaries for algorithms and computation -- Software and hardware verification and testing -- Conclusion.

The philosophy of mathematics has long been concerned with deter- mining the means that are appropriate for justifying claims of mathemat- ical knowledge, and the metaphysical considerations that render them so. But, as of late, many philosophers have called attention to the fact that a much broader range of normative judgments arise in ordinary math- ematical practice; for example, questions can be interesting, theorems important, proofs explanatory, concepts powerful, and so on. The as- sociated values are often loosely classied as (...) aspects of \mathematical understanding." Meanwhile, in a branch of computer science known as \formal ver- ication," the practice of interactive theorem proving has given rise to software tools and systems designed to support the development of com- plex formal axiomatic proofs. Such eorts require one to develop models of mathematical language and inference that are more robust than the the simple foundational models of the last century. This essay explores some of the insights that emerge from this work, and some of the ways that these insights can inform, and be informed by, philosophical theories of mathematical understanding. (shrink)

This paper provides a review of Raymond Turner’s book Computational Artefacts. Towards a Philosophy of Computer Science. Focus is made on the definition of program correctness as the twofold problem of evaluating whether both the symbolic program and the physical implementation satisfy a set of specifications. The review stresses how these are not two separate problems. First, it is highlighted how formal proofs of correctness need to rely on the analysis of physical computational processes. Secondly, it is underlined how (...) software testing requires considering the formal relations holding between the specifications and the symbolic program. Such a mutual dependency between formal and empirical program verification methods is finally shown to influence the debate on the epistemological status of computer science. (shrink)

This festschrift volume is dedicated to Boris (Boaz) Trakhtenbrot on the occasion of his 85th birthday. For over half a century, Trakhtenbrot has been making seminal contributions to virtually all of the central areas of theoretical computer science. He is universally admired as a founding father and long-standing pillar of the discipline of computer science. On Friday, 28 April 2006, the School of Computer Science at Tel Aviv University held a “Computation Day Celebrating Boaz (Boris) Trakhtenbrot's Eighty-Fifth (...) Birthday”. As a follow-up to that event, his students and colleagues were asked to contribute to a volume in his honor and in recognition of his grand contributions to the field. The book opens with two historical overviews and a bibliography. These are followed by 33 thoroughly reviewed technical contributions. The broad range of topics covered include mathematical logic, logics for computer science, mathematics for computer science, automata and formal languages, asynchronous computation, semantics of programming languages, verification, and software engineering. This tapestry of subjects stands as testimony to the vast scope of Trakhtenbrot's achievements and the profound influence he has had on the field. (shrink)

‘It is much more difficult than is often admitted to make a strong case for the ownership of computer software.’ This closely argued study of the strengths and weaknesses of the case for intellectual property rights and against software piracy is based on material contained in the author’s joint work with Douglas Adeney, Computer and Information Ethics, Greenwood Press, an imprint of Greenwood Publishing Group, INC., Westport, CT, forthcoming May, 1997. The author is a member of (...) the School of Information Studies at Charles Sturt University, PO Box 588, Wagga Wagga, NSW 2650 Australia; tel 61 69 33 2372; fax 61 69 33 2733; email [email protected] wishes to acknowledge the contribution to this paper of Douglas Adeney of the University of Melbourne. (shrink)

Designing and building complex artifacts like simulation models often rely on the strategy of modularity. My main claim is that the validation of simulation models faces a challenge of holismHolism because modularityModularity tends to erode over the process of building a simulation model. Two different reasons that fuel the tendency to erosion are analyzed. Both are based on the methodologyMethodology of simulation, but on different levels. The first has to do with the way parameter adjustment works in simulation; the second (...) comes from how different groups of software programmers work together. The chapter will conclude by drawing lessons about how holism challenges the validation of simulation and by discussing a corollary to conformational holism: the boundary between validation and verification tends to become blurred, thus undermining a strategy that insists on keeping them separate. (shrink)

‘It is much more difficult than is often admitted to make a strong case for the ownership of computer software.’ This closely argued study of the strengths and weaknesses of the case for intellectual property rights and against software piracy is based on material contained in the author’s joint work with Douglas Adeney, Computer and Information Ethics, Greenwood Press, an imprint of Greenwood Publishing Group, INC., Westport, CT, forthcoming May, 1997. The author is a member of (...) the School of Information Studies at Charles Sturt University, PO Box 588, Wagga Wagga, NSW 2650 Australia; tel 61 69 33 2372; fax 61 69 33 2733; email [email protected] wishes to acknowledge the contribution to this paper of Douglas Adeney of the University of Melbourne. (shrink)

. Computational chemistry grew in a new era of “desktop modeling,” which coincided with a growing demand for modeling software, especially from the pharmaceutical industry. Parameterization of models in computational chemistry is an arduous enterprise, and we argue that this activity leads, in this specific context, to tensions among scientists regarding the epistemic opacity transparency of parameterized methods and the software implementing them. We relate one flame war from the Computational Chemistry mailing List in order to assess in (...) detail the relationships between modeling methods, parameterization, software and the various forms of their enclosure or disclosure. Our claim is that parameterization issues are an important and often neglected source of epistemic opacity and that this opacity is entangled in methods and software alike. Models and software must be addressed together to understand the epistemological tensions at stake. (shrink)

Interactive theorem provers might seem particularly impractical in the history of philosophy. Journal articles in this discipline are generally not formalized. Interactive theorem provers involve a learning curve for which the payoffs might seem minimal. In this article I argue that interactive theorem provers have already demonstrated their potential as a useful tool for historians of philosophy; I do this by highlighting examples of work where this has already been done. Further, I argue that interactive theorem provers can continue to (...) be useful tools for historians of philosophy in the future; this claim is defended through a more conceptual analysis of what historians of philosophy do that identifies argument reconstruction as a core activity of such practitioners. It is then shown that interactive theorem provers can assist in this core practice by a description of what interactive theorem provers are and can do. If this is right, then computer verification for historians of philosophy is in the offing. (shrink)

This book constitutes the refereed proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011, held in Ann Arbor, MI, USA in June 2011.The 25 revised full papers presented together with ...

Quantum computing is of high interest because it promises to perform at least some kinds of computations much faster than classical computers. Arute et al. 2019 (informally, “the Google Quantum Team”) report the results of experiments that purport to demonstrate “quantum supremacy” – the claim that the performance of some quantum computers is better than that of classical computers on some problems. Do these results close the debate over quantum supremacy? We argue that they do not. In the following, we (...) provide an overview of the Google Quantum Team’s experiments, then identify some open questions in the quest to demonstrate quantum supremacy. (shrink)

In this paper I attempt to cast the current program verification debate within a more general perspective on the methodologies and goals of computer science. I show, first, how any method involved in demonstrating the correctness of a physically executing computer program, whether by testing or formal verification, involves reasoning that is defeasible in nature. Then, through a delineation of the senses in which programs can be run as tests, I show that the activities of testing (...) and formal verification do not necessarily share the same goals and thus do not always constitute alternatives. The testing of a program is not always intended to demonstrate a program's correctness. Testing may seek to accept or reject nonprograms including algorithms, specifications, and hypotheses regarding phenomena. The relationship between these kinds of testing and formal verification is couched in a more fundamental relationship between two views of computer science, one properly containing the other. (shrink)

in Oct-14-1998 ordinance INDESP-IO4 established the federal software certification and verification requirements for gaming machines in Brazil. The authors present the rationale behind these criteria, whose basic principles can find applications in several other software authentication applications.

Verification and validation of computer codes and models used in simulation are two aspects of the scientific practice of high importance and have recently been discussed by philosophers of science. While verification is predominantly associated with the correctness of the way a model is represented by a computer code or algorithm, validation more often refers to model’s relation to the real world and its intended use. It has been argued that because complex simulations are generally not (...) transparent to a practitioner, the Duhem problem can arise for verification and validation due to their entanglement; such an entanglement makes it impossible to distinguish whether a coding error or model’s general inadequacy to its target should be blamed in the case of the model failure. I argue that in order to disentangle verification and validation, a clear distinction between computer modeling and simulation needs to be made. Holding on to that distinction, I propose to relate verification to modeling and validation, which shares the common epistemology with experimentation, to simulation. To explain reasons of their intermittent entanglement I propose a weberian ideal-typical model of modeling and simulation as roles in practice. I suggest an approach to alleviate the Duhem problem for verification and validation generally applicable in practice and based on differences in epistemic strategies and scopes. (shrink)

Computational reproducibility possesses its own dynamics and narratives of crisis. Alongside the difficulties of computing as an ubiquitous yet complex scientific activity, computational reproducibility suffers from a naive expectancy of total reproducibility and a moral imperative to embrace the principles of free software as a non-negotiable epistemic virtue. We argue that the epistemic issues at stake in actual practices of computational reproducibility are best unveiled by focusing on software as a pivotal concept, one that is surprisingly often overlooked (...) in accounts of reproducibility issues. Software is not only about designing and coding but also about maintaining, supporting, distributing, licensing, and governance; it is not only about developers but also about users. We focus on openness debates among computational chemists involved in molecular modeling software packages as empirical grounding for our argument. We then identify and analyse four epistemic characteristics as key to the role of software in computational reproducibility. (shrink)

Proof and Disproof in Formal Logic is a lively and entertaining introduction to formal logic providing an excellent insight into how a simple logic works. Formal logic allows you to check a logical claim without considering what the claim means. This highly abstracted idea is an essential and practical part of computer science. The idea of a formal system-a collection of rules and axioms, which define a universe of logical proofs-is what gives us programming languages and modern-day programming. This (...) book concentrates on using logic as a tool: making and using formal proofs and disproofs of particular logical claims. The logic it uses-natural deduction-is very small and very simple; working with it helps you see how large mathematical universes can be built on small foundations. The book is divided into four parts: Part I "Basics" gives an introduction to formal logic with a short history of logic and explanations of some technical words. Part II "Formal Syntactic Proof" show you how to do calculations in a formal system where you are guided by shapes and never need to think about meaning. Your experiments are aided by Jape, which can operate as both inquisitor and oracle. Part III "Formal Semantic Disproof" shows you how to construct mathematical counterexamples to shoe that proof is impossible. Jape can check the counterexamples you build. Part IV " Program Specification and Proof" describes how to apply your logical understanding to a real computer science problem, the accurate description and verification of programs. Jape helps, as far as arithmetic allows. Aimed at undergraduates and graduates in computer science, logic, mathematics and philosophy, the text includes reference to and exercises based on the computer software package Jape, an interactive teaching and research tool designed and hosted by the author that is freely available on the web. (shrink)

This commentary on John Symons’ and Jack Horner’s paper, besides sharing its main argument, challenges the authors’ statement that there is no effective method to evaluate software-intensive systems as a distinguishing feature of software intensive science. It is underlined here how analogous methodological limitations characterise the evaluations of empirical systems in non-software intensive sciences. The authors’ claim that formal methods establish the correctness of computational models rather than of the represented programme is here compared with the empirical (...) adequacy problem typifying the model-based reasoning approach in physics, and the remark that testing all the paths of a software-intensive system is unfeasible is related to the enumerative induction problem in the justification of empirical law-like hypotheses in non-software intensive sciences. (shrink)

Verification and validation of computer codes and models used in simulations are two aspects of the scientific practice of high importance that recently have been discussed widely by philosophers of science. While verification is predominantly associated with the correctness of the way a model is represented by a computer code or algorithm, validation more often refers to the model’s relation to the real world and its intended use. Because complex simulations are generally opaque to a practitioner, (...) the Duhem problem can arise with verification and validation due to their entanglement; such an entanglement makes it impossible to distinguish whether a coding error or the model’s general inadequacy to its target should be blamed in the case of a failure. I argue that a clear distinction between computer modeling and simulation has to be made to disentangle verification and validation. Drawing on that distinction, I suggest to associate modeling with verification and simulation, which shares common epistemic strategies with experimentation, with validation. To explain the reasons for their entanglement in practice, I propose a Weberian ideal–typical model of modeling and simulation as roles in practice. I examine an approach to mitigate the Duhem problem for verification and validation that is generally applicable in practice and is based on differences in epistemic strategies and scopes. Based on this analysis, I suggest two strategies to increase the reliability of simulation results, namely, avoiding alterations of verified models at the validation stage as well as performing simulations of the same target system using two or more different models. In response to Winsberg’s claim that verification and validation are entangled I argue that deploying the methodology proposed in this work it is possible to mitigate inseparability of V&V in many if not all domains where modeling and simulation are used. (shrink)

For over 50 years, since the development of nuclear-armed ICBMs, the USA has sought a way to defend against them. These efforts evolved through various strategies and technologies: from nuclear-tipped rockets through space-based laser weapons to today’s system of ground-based kinetic-kill interceptors. Public debate around these issues reached a peak in the 1980s with President Reagan’s Strategic Defense Initiative, popularly known as Star Wars.Rebecca Slayton examines this history in Arguments that Count, a valuable and well-told account of a particular aspect (...) of missile defense: computer software. Missile defense required identifying a hostile missile launch, keeping track of thousands of incoming warheads on their ballistic trajectories, and directing interceptors to the right place—and doing all this in less than 30 minutes. From the outset, designers turned to computers to do the complex calculations quickly enough. But missile defense presented an additional factor, in that any m .. (shrink)

Software piracy is older than the PC and has been the subject of several studies, which have found it to be a widespread phenomenon in general, and among university students in particular. An earlier study by Cohen and Cornwell from a decade ago is replicated, adding questions about downloading music from the Internet. The survey includes responses from 224 students in entry-level courses at two schools, a nondenominational suburban university and a Catholic urban college with similar student profiles. The (...) study found that there has been few if any changes in student opinions regarding the unauthorized duplication of copy- righted materials. Students generally felt that copying commercial software and downloading music from the Internet was acceptable and found that there was no significant correlation between student attitudes and their school’s religious affiliation or lack thereof. Additionally, the study found that a small but significant percentage of respondents considered the other questionable behaviors as ethically acceptable. Finally, the reasons for these attitudes are discussed as well as what colleges can do to correct the situation. (shrink)

Computation of seismic parameters and its interpretation from the recorded earthquake signal is empowered by digital data acquisition systems. This enables seismologist to automatically compute all the relevant parameters. Futuristic applications require extensive software development to implement seismic prediction and forecasting models. While developing such models, software developer prefer to write their own in-house analysis & modeling software with complete control over the required computations and models. This paper presents simplified mathematical framework of the seismic events and (...) back-end computational software logic & algorithm to provide a simple framework to software engineers develop customized seismic analysis & computation software. (shrink)

Defending or attacking either functionalism or computationalism requires clarity on what they amount to and what evidence counts for or against them. My goal here is not to evaluate their plausibility. My goal is to formulate them and their relationship clearly enough that we can determine which type of evidence is relevant to them. I aim to dispel some sources of confusion that surround functionalism and computationalism, recruit recent philosophical work on mechanisms and computation to shed light on them, and (...) clarify how functionalism and computationalism may or may not legitimately come together. (shrink)

To study the static software defect detection system, based on the traditional static software defect detection system design, a new static software defect detection system design based on big data technology is proposed. The proposed method can optimize the distribution of test resources and improve the quality of software products by predicting the potential defect program modules and design the software and hardware of the static software defect detection system of big data technology. It (...) is found that the traditional static software defect detection system design based on code source data takes a long time, averaging 65 h /day. However, the traditional static software defect detection system based on deep learning has a short detection time, averaging 35 h/day. In this article, the detection time of the static software defect detection system based on big data is shorter than that of the other two traditional system designs, with an average of 15 h/day. Because the system design adjusts the operating state of the system, it improves the accuracy of data operation. On the premise of data collection, the system inspection research is completed, which ensures the operational safety of software data, alleviates the contradiction between system and data to a high degree, improves the efficiency of system operation, reduces unnecessary operations, further shortens the time required for inspection, improves the system performance, and has higher research and operation value. (shrink)