Program Verification Using Higher Order Logic
ELECTRONICS RESEARCH LAB ADELAIDE (AUSTRALIA)
Pagination or Media Count:
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 Programming and Software