Software Verification

This is an introduction to the Isabelle proof assistant aimed at philosophers and their students.

As the Life Insurance industry undergoes rapid digital transformation, the need for more intelligent and adaptive testing methods has become crucial. Traditional test case generation methods often struggle to keep pace with the industry’s dynamic requirements, intricate processes, and evolving regulatory landscapes. In this context, Generative AI (GenAI) is emerging as a game-changer, bringing a new level of efficiency, scalability, and intelligence to software quality assurance. This paper delves into the application of GenAI for autonomous test case generation in life (...) insurance applications, exploring how it can streamline testing, enhance accuracy, and reduce manual effort. Through comparisons with traditional approaches, real-world case studies, and a discussion of best practices, we uncover the tangible benefits and challenges of adopting GenAI in this domain. Additionally, the paper sheds light on future possibilities, aiming to inspire innovation and drive further advancements in quality assurance for life insurance systems. (shrink)

As the financial services industry advances, managing the inherent complexities of annuities requires sophisticated risk management in software testing. Traditional methodologies are insufficient to address the multi-dimensional challenges posed by evolving regulatory landscapes, intricate financial models, and system integration. This paper investigates the application of Artificial Intelligence (AI) and Machine Learning (ML) to enhance risk mitigation across critical testing domains, including compliance automation, financial accuracy, data security, and performance optimization. AI/ML technologies introduce advanced automation, predictive analytics, and anomaly detection, elevating (...) the precision and efficiency of the testing lifecycle. Through continuous learning models and adaptive testing frameworks, AI/ML streamlines legacy system integrations and dynamically scales performance testing. This article establishes the strategic imperative for insurers to integrate AI/ML into software testing frameworks, ensuring a proactive, data-driven approach to risk management and future-proofing their technological ecosystems. (shrink)

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)

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)

Una imagen muy generalizada a la hora de entender el software de computador es la que lo representa como una “caja negra”: no importa realmente saber qué partes lo componen internamente, sino qué resultados se obtienen de él según ciertos valores de entrada. Al hacer esto, muchos problemas filosóficos son ocultados, negados o simplemente mal entendidos. Este artículo discute tres unidades de análisis del software de computador, esto es, las especificaciones, los algoritmos y los procesos computacionales. El objetivo central es (...) entender las prácticas cientficas e ingenieriles detrás de cada unidad de software, así como analizar su metodología, ontología y epistemología. (shrink)

The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.

Artefacts do not always do what they are supposed to, due to a variety of reasons, including manufacturing problems, poor maintenance, and normal wear-and-tear. Since software is an artefact, it should be subject to malfunctioning in the same sense in which other artefacts can malfunction. Yet, whether software is on a par with other artefacts when it comes to malfunctioning crucially depends on the abstraction used in the analysis. We distinguish between “negative” and “positive” notions of malfunction. A negative malfunction, (...) or dysfunction, occurs when an artefact token either does not or cannot do what it is supposed to. A positive malfunction, or misfunction, occurs when an artefact token may do what is supposed to but, at least occasionally, it also yields some unintended and undesirable effects. We argue that software, understood as type, may misfunction in some limited sense, but cannot dysfunction. Accordingly, one should distinguish software from other technical artefacts, in view of their design that makes dysfunction impossible for the former, while possible for the latter. (shrink)

Interest in the computational aspects of modeling has been steadily growing in philosophy of science. This paper aims to advance the discussion by articulating the way in which modeling and computational errors are related and by explaining the significance of error management strategies for the rational reconstruction of scientific practice. To this end, we first characterize the role and nature of modeling error in relation to a recipe for model construction known as Euler’s recipe. We then describe a general model (...) that allows us to assess the quality of numerical solutions in terms of measures of computational errors that are completely interpretable in terms of modeling error. Finally, we emphasize that this type of error analysis involves forms of perturbation analysis that go beyond the basic model-theoretical and statistical/probabilistic tools typically used to characterize the scientific method; this demands that we revise and complement our reconstructive toolbox in a way that can affect our normative image of science. (shrink)

Automated Software Testing (AST) using Model Checking is in this article epistemologically analysed in order to argue in favour of a model-based reasoning paradigm in computer science. Preliminarily, it is shown how both deductive and inductive reasoning are insufficient to determine whether a given piece of software is correct with respect to specified behavioural properties. Models algorithmically checked in Model Checking to select executions to be observed in Software Testing are acknowledged as analogical models which establish isomorphic relations with the (...) target system’s data set. Analogical models developed in AST are presented as abductive models providing hypothetical explanations to observed executions. The model assumption—algorithmic check—software testing process is understood as the abduction—deduction—induction process defining the selective abduction and turned to isolate a set of model-based hypotheses concerning the target system behaviours. A manipulative abduction process is finally recognized in the practice of adapting, abstracting and refining models that do not provide successful predictions. (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)

The terms ‘verification’ and ‘validation’ are widely used in science, both in the natural and the social sciences. They are extensively used in simulation, often associated with the need to evaluate models in different stages of the simulation development process. Frequently, terminological ambiguities arise when researchers conflate, along the simulation development process, the technical meanings of both terms with other meanings found in the philosophy of science and the social sciences. This article considers the problem of verification and validation in (...) social science simulation along five perspectives: The reasons to address terminological issues in simulation; the meaning of the terms in the philosophical sense of the problem of “truth”; the observation that some debates about these terms in simulation are inadvertently more terminological than epistemological; the meaning of the terms in the technical context of the simulation development process; and finally, a comprehensive outline of the relation between terminology used in simulation, different types of models used in the development process and different epistemological perspectives. (shrink)

The formal and empirical-generative perspectives of computation are demonstrated to be inadequate to secure the goals of simulation in the social sciences. Simulation does not resemble formal demonstrations or generative mechanisms that deductively explain how certain models are sufficient to generate emergent macrostructures of interest. The description of scientific practice implies additional epistemic conceptions of scientific knowledge. Three kinds of knowledge that account for a comprehensive description of the discipline were identified: formal, empirical and intentional knowledge. The use of formal (...) conceptions of computation for describing simulation is refuted; the roles of programming languages according to intentional accounts of computation are identified; and the roles of iconographic programming languages and aesthetic machines in simulation are characterized. The roles that simulation and intentional decision making may be able to play in a participative information society are also discussed. (shrink)

This article reports an exploratory survey of the structure of interdisciplinary research in Agent-Based Social Simulation. One hundred and ninety six researchers participated in the survey completing an on-line questionnaire. The questionnaire had three distinct sections, a classification of research domains, a classification of models, and an inquiry into software requirements for designing simulation platforms. The survey results allowed us to disambiguate the variety of scientific goals and modus operandi of researchers with a reasonable level of detail, and to identify (...) a classification of agent-based models used in simulation. In particular, in the interdisciplinary context of social-scientific modelling, agent-based computational modelling and computer engineering, we analyse the extent to which these paradigmatic models seem to be mutually instrumental in the field. We expect that our proposal may improve the viability of submitting, explaining and comparing agent-based simulations in articles, which is an important methodological requirement to consolidate the field. We also expect that it will motivate other proposals that could further validate, extend or change ours, in order to refine the classification with more types of models. (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.

The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.

RIC VERIFY defines deterministic decision verification infrastructure. It replaces logs and explanations with replayable, signed artifacts that can be independently verified offline. This paper specifies the minimal requirements for verifiable decision systems and establishes verification as a required layer for consequential AI.

This lecture proposes a structural map of artificial intelligence and the infrastructure that becomes necessary once AI systems produce consequential decisions. It begins with three foundational questions: recognition asks what class an input belongs to; generation asks what continuation could follow; representation asks what remains invariant under transformation. The lecture then traces a representation-learning lineage from convolutional networks through Siamese networks, contrastive learning, BYOL, Barlow Twins, VICReg, and JEPA, interpreting this lineage as a progressive operationalization of identity under change. -/- (...) The second half of the lecture argues that conventional AI diagrams stop too early. Once AI systems move from prediction into consequential action, additional accountability layers become necessary: verification, federated settlement, proof-gated execution, and persistent governance. These layers convert decisions from transient model outputs into replayable, independently verifiable artifacts capable of supporting audit, dispute resolution, authorization, and long-term governance. The central claim is not that every AI system requires every layer, but that as consequence increases, systems require stronger mechanisms for preserving and proving sameness across transformation. -/- The lecture is offered as a conceptual map rather than a formal proof. Its lower sections summarize established developments in machine learning; its upper sections describe emerging infrastructure and architectural proposals for consequential AI systems. (shrink)

This paper argues that increasingly autonomous AI systems require a new evidentiary primitive beyond conventional observability. Logs, traces, metrics, and audit events explain how software executed but do not necessarily preserve the consequential decision itself as an independently verifiable object. The paper introduces the concept of the decision object: a canonical artifact created at runtime that packages the evidence boundary, governing policy, authority chain, decision output, and cryptographic commitment required for later verification. This yields a shift from reconstructing decisions after (...) the fact toward verifying them under declared regimes. The paper distinguishes decision proof from observability, develops the architectural consequences of runtime decision objects, and argues that decision proof constitutes a distinct infrastructure layer for governance, regulation, appeals, adjudication, and institutional trust. VERIFY is presented as a reference implementation of the broader architectural category rather than as the subject of the paper. (shrink)

This paper introduces an evaluation framework for persistent autonomous systems, building on prior work defining their structure and enforcement. A system must not only satisfy identity persistence, bounded drift, and replay-verifiable action in principle; it must be demonstrably compliant under structured testing. -/- We define PAS compliance criteria and introduce test protocols for identity persistence, drift governance, replay verification, and continuous enforcement. Systems are evaluated through failure diagnostics and classified across levels of compliance, from non-compliant to PAS-compliant. -/- The result (...) is a practical evaluation standard that converts theoretical requirements into testable conditions. Autonomy is not assumed from capability; it is demonstrated through reproducible evidence that a system persists as the same lawful subject across time. (shrink)

This paper develops a mathematical theory of identity persistence under admissible transformation. It asks what structure is required for a same/not-same judgment across recurrence to be meaningful, non-arbitrary, and non-trivial. The theory defines identity-bearing units, state spaces, admissible transformations, admissible redescriptions, quotient state spaces, continuation relations, invariant vectors, scalar governance functionals, drift bounds, verdict functions, and finite-state identity capacity. -/- The central claim is structural rather than ontological: a persistence judgment is coherent only when the identity-bearing unit, admissible transformation regime, (...) quotient, invariant basis, continuation structure, governance rule, and drift bounds are specified. The paper introduces a finite verdict set: PERSIST, BREAK, BRANCH, UNDEFINED, and REGIME-CHANGE. -/- It also introduces C_I, a finite-state capacity quantity defined as the asymptotic logarithmic growth rate of admissible identity-preserving trajectories in a finite admissibility graph. In local finite regimes, C_I is given by the logarithm of the spectral radius of the admissible-transition matrix. For path-budget constraints, the state space is lifted to include accumulated drift. -/- The result does not settle ontology or replace probability, entropy, or communication theory. It supplies a formal framework for when “same system” claims are well-defined, plus a graph-theoretic measure of how many identity-preserving transformations a declared regime allows. (shrink)

This note argues that many disputes concerning identity, persistence, explanation, knowledge, verification, and governance share a common structural failure: evaluation is attempted before the conditions required for evaluation have been declared. It develops a methodological template derived from the identity–persistence program. On this template, a judgment becomes admissible only relative to a declared evaluation regime specifying the object, authority, admissible transformations, admissible redescriptions, invariants, continuation conditions, drift bounds, proof obligations, and re-verification conditions. The note does not decide which evaluation regimes (...) are correct, nor does it offer ontological closure. Its aim is narrower: to determine whether a claim has become a coherent object of evaluation. The central principle is that admissibility precedes verdict. (shrink)

Consequential AI systems increasingly depend upon claims that decisions, tasks, authorities, policies, memories, and artifacts remain the same across transformation. This paper develops an applied architecture for those claims by instantiating the Identity–Persistence Program’s forcing theorems within AI systems rather than extending the underlying formal theory. -/- The proposed architecture separates probabilistic discovery from deterministic adjudication. Probabilistic components estimate candidate regimes and generate candidate continuations, while deterministic identity kernels evaluate persistence under declared regimes before proof gates license consequential action. The (...) resulting inversion shifts optimization from search toward bounded adjudication under explicit structural assumptions. -/- Identity kernels, governed memory, retraction propagation, runtime admission, federation, and persistent governance are presented as coordinated architectural components operating over declared regimes. Seven regime templates demonstrate how the same forced structural roles instantiate across distinct classes of consequential AI persistence claims while preserving strict separation between formal results, engineering embodiments, and empirical questions. -/- The paper argues that identity enforcement constitutes an architectural category distinct from observability, evaluation, provenance, or governance tooling. Throughout, claims are explicitly bounded: PASS denotes licensed admissibility under a declared regime rather than truth; hallucinations are not prevented but prevented from becoming consequential when they fail declared admission criteria; and the architecture remains silent on ontological questions outside its declared scope. The result is an applied framework for governing consequential AI through deterministic identity enforcement over probabilistic generation. (shrink)

A data provenance framework is subject to security threats and risks, which increase the uncertainty, or lack of trust, in provenance information. Information assurance is challenged by incomplete information; one cannot exhaustively characterize all threats or all vulnerabilities. One technique that specifically incorporates a probabilistic notion of uncertainty is subjective logic. Subjective logic allows belief and uncertainty, due to incomplete information, to be specified and operated upon in a coherent manner. A mapping from the standard definition of information assurance to (...) a more quantitative subjective logic framework is suggested with a focus on the specific application of data provenance. Finally, specific consideration is given to the notion of uncertainty within subjective logic and its relation to information entropy. Information entropy is an alternative measure of uncertainty and a fundamental relationship is hypothesized between uncertainty in subjective logic and entropy. (shrink)