Program Verification Using Higher Order Logic.

摘要

This paper describes a number of experiments in program verification carried out within two automated proof assistants, namely the HOL (High Order Logic) system and Isabelle. Various approaches to programming language semantics are described. Theories and tactics for proving the correctness of programs written in small functional and imperative languages are then constructed within HOL and Isabelle. Computer program verification, High level language, Semantics, Logic Programming.