Abstract

We present a hybrid approach to program verification: a higher-order logic, used as a specification language, and a human-driven proof environment, with a process-algebraic engine to allow the use of process simulation as an abstraction technique. The domain of application is the validation of object code, and our intent is to adapt and mix existing formalisms to make the verification of representative programs possible. In this paper, we describe the logic in question and an underlying semantics given in terms of a process algebra.

Keywords: formal verification, higher-order logic, process algebra, automated theorem prover

Full paper: [ps - 205 KB] [ps.gz - 80 KB] [pdf - 164 KB].