Program verification by symbolic execution of hyperfinite ideal machines. (English) Zbl 0786.68066
Computer-aided verification ’90, Proc. 2nd DIMACS Workshop, New Brunswick/NJ (USA) 1990, DIMACS, Ser. Discret. Math. Theor. Comput. Sci. 3, 441-462 (1991).
Summary: [For the entire collection see Zbl 0753.00020.]
Ariel, a program verification system based on symbolic execution and non- standard analysis, is described. Programs are verified by showing that the traces resulting from their execution on a hyperfinite abstract interpreter satisfy their specifications. An Ariel abstract interpreter is written in a functional programming language, Caliban, for which we have a theorem prover. Caliban is similar to Miranda. Ariel is especially useful for verifying programs that compute with real numbers. The real data type of an Ariel abstract interpreter is taken to be a hyperfinite subset of the non-standard reals. The imprecision of real arithmetic is modelled by assuming that real arithmetic operations compute results that differ from the ideal ones by an infinitesimal. Programs are required to compute results that differ by an infinitesimal from the ideal. Programs that have this property are said to be asymptotically correct. If a program is asymptotically correct, then it can be shown that there exists a sufficiently precise machine on which the program can be run to obtain results of a desired accuracy. The theory does not predict how accurate that machine has to be to achieve the desired results, but does provide a means of verification that catches a large number of programming errors. A prototype Ariel system has been built and is in use.
Ariel, a program verification system based on symbolic execution and non- standard analysis, is described. Programs are verified by showing that the traces resulting from their execution on a hyperfinite abstract interpreter satisfy their specifications. An Ariel abstract interpreter is written in a functional programming language, Caliban, for which we have a theorem prover. Caliban is similar to Miranda. Ariel is especially useful for verifying programs that compute with real numbers. The real data type of an Ariel abstract interpreter is taken to be a hyperfinite subset of the non-standard reals. The imprecision of real arithmetic is modelled by assuming that real arithmetic operations compute results that differ from the ideal ones by an infinitesimal. Programs are required to compute results that differ by an infinitesimal from the ideal. Programs that have this property are said to be asymptotically correct. If a program is asymptotically correct, then it can be shown that there exists a sufficiently precise machine on which the program can be run to obtain results of a desired accuracy. The theory does not predict how accurate that machine has to be to achieve the desired results, but does provide a means of verification that catches a large number of programming errors. A prototype Ariel system has been built and is in use.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03H10 | Other applications of nonstandard models (economics, physics, etc.) |
| 65G99 | Error analysis and interval analysis |
