Ariel swMATH ID: 24050 Software Authors: Morris, James M.; Howard, Mark Description: Program verification by symbolic execution of hyperfinite ideal machines. (Extended abstract). This paper describes Ariel, a program verification system based on the symbolic execution of hyperfinite ideal machines.par A hyperfinite ideal machine is a transition system in which some of the components of terms are defined using constructs from non-standard analysis. The original version of Ariel was designed primarily for the verification of numerical programs written in a subset of C. We formulated a notion of correctness of numerical programs, called asymptotic correctness, using concepts from non-standard analysis. This led to the formulation of non-standard models of computation which have proved to be of general utility in program verification.par By ideal machine we mean a transition system that gives an operational semantics for the language in which the programs we wish to verify are written. The terms of a transition system can be thought of as the states of an ideal machine, tailored to the language in question, which executes the program to be verified. The meaning of the program is identified with the execution traces of the transition system or ideal machine. A program is verified by showing that its traces satisfy its specification. The transition systems are defined in an applicative programming language for which we have a theorem prover. This applicative language, called Caliban, is lazy, higher-order, and polymorphic. The theorem prover, called Clio, provides a meta-language for making assertions about the meanings of Caliban terms. One can write a Caliban expression whose meaning is the trace of a (sub-)program beginning in some initial state. The pre- and postconditions that the initial and final states of such a trace respectively are to satisfy are written in Clio’s meta-language. A (sub-)program is verified by using Clio to show that its precondition implies its postcondition. Clio’s proof rule for implication attempts to prove the postcondition under assumption of the precondition. Homepage: https://rd.springer.com/chapter/10.1007/BFb0023746 Keywords: program verification system; transition system; verification of numerical programs; asymptotic correctness Related Software: Caliban; Clio; Miranda Cited in: 2 Documents Cited by 2 Authors 2 Howard, Mark 2 Morris, James M. Cited in 0 Serials Cited in 3 Fields 2 Numerical analysis (65-XX) 2 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year