Accession Number : ADA255408


Title :   Program Verification Using Higher Order Logic


Descriptive Note : Research rept.,


Corporate Author : ELECTRONICS RESEARCH LAB ADELAIDE (AUSTRALIA)


Personal Author(s) : Cant, A


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a255408.pdf


Report Date : Jan 1992


Pagination or Media Count : 92


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.


Descriptors :   *COMPUTER PROGRAM VERIFICATION , COMPUTER PROGRAMS , COMPUTERS , COMPUTER PROGRAMMING , NUMBERS , HIGH LEVEL LANGUAGES , APPROACH , LOGIC , PROGRAMMING LANGUAGES , SEMANTICS , LANGUAGE


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE