Formal Numerical Program Analysis
William M. Farmer, F. Javier Thayer · 2002
This paper describes a method for formally analyzing numerical programs and a software system that implements the method. The software system translates a purely functional Pre-Scheme program that manipulates machine integers into a representation in the imps Interactive Mathematical Proof System. The correctness of the Pre-Scheme program is analyzed by stating and proving conjectures about the imps representation using the imps theorem proving facility. This work was carried out in FY94 under MITRE's System Security Analysis project (project number: 8360; sponsor: NSA/C62). Contents 1 Introduction 1 2 Pre-Scheme 2 3 IMPS 3 4 The IMPS Theory of Machine Arithmetic 4 5 The Pre-Scheme-to-IMPS Translator 5 6 Examples 7 6.1 Even and Odd Testers . . . . . . . . . . . . . . . . . . . . . . 8 6.1.1 The Pre-Scheme Program . . . . . . . . . . . . . . . . 8 6.1.2 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . 8 6.2 Recursive Factorial Function . . . . . . . . . . . . . . ....