Towards a Discipline for Developing Verified Software

William M. Farmer, Dale M. Johnson, F. Javier Thayer

1986

Abstract

In this paper the formal verification of computer systems and software
is viewed as an endeavor in applied mathematics.  It is argued that a
formal verification should consist of three separate but interacting
processes: a modelling process, a theorem proving process, and a
review and acceptance process.  Suggestions are made for improving the
development of these processes.  Taken together, they outline a
proposed discipline for the development of verified software.  The
ideas presented were principally, though not exclusively, motivated by
the authors' work in reviewing the design verification of the
Restricted Access Processor (RAP).  Examples are drawn from the RAP
verification to support our suggestions for improving formal
verification.