Accession Number:

ADA255408

Title:

Program Verification Using Higher Order Logic

Descriptive Note:

Research rept.,

Corporate Author:

ELECTRONICS RESEARCH LAB ADELAIDE (AUSTRALIA)

Personal Author(s):

Report Date:

1992-01-01

Pagination or Media Count:

92.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE