Program Verification Using Higher Order Logic

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1992
Accession Number
ADA255408

Entities

People

  • A. Cant

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Command And Control
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Engineering
  • Grammars
  • High Level Languages
  • Information Processing
  • Information Systems
  • Language
  • Notation
  • Programming Languages
  • Recursive Functions
  • Software Development

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.