Formal Specification and Verification in HOL

Higher Order Logic, or HOL, is a widely-used tool for creating formal specifications of systems, and for proving properties about them. It has been used in both industry and academia to support formal reasoning in many areas, including hardware and software verification. The underlying logic and basic facilities are completely general. In principle they can be used to support any project which can be defined in higher order logic, an expressive logic originally developed as a foundation for mathematics.

Welcome to the HOL home page, describing the formal specification research using HOL underway in the Penn Department of Computer and Information Science and Bell Labs and AT&T as well as pointers to related material.

Projects

• HOL90: An HOL system based on Standard ML. (Tutorial.)
• Sunrise: A Verified Verification Condition Generator
• Higher Order Quotients: A design and implementation for higher order quotients in higher order logic.
• The Village Telephone System: An experiment in using HOL to capture requirements.

People

• Carl A. Gunter
• Peter Homeier
• Pamela Zave
• Michael Jackson
• Karthikeyan Bhargavan
• Elsa L. Gunter
• Davor Obradovic

Papers

Formal Verification of Standards for Distance Vector Routing
Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter

A Reference Model for Requirements and Specifications
Carl A. Gunter, Elsa L. Gunter, Michael Jackson, and Pamela Zave.

The Village Telephone System: A Case Study in Formal Software Engineering
Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, and Pamela Zave.

Infrastructure for Proof-Referencing Code
Carl A. Gunter, Peter Homeier, and Scott Nettles. International Conference on Theorem Proving in Higher Order Logics.

Sunrise:

• Mechanical Verification of Total Correctness Through Diversion Verification Conditions. (PDF), with briefing, (PDF)

Peter V. Homeier and David F. Martin.
Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98), eds. J. Grundy and M. Newey, The Australian National University (ANU), Canberra, Australia, September 28 - October 1, 1998. Lecture Notes in Computer Science Vol 1479, Springer-Verlag, pages 189-206.
• Mechanical Verification of Mutually Recursive Procedures. (PDF)

Peter V. Homeier and David F. Martin.
Proceedings of the 13th International Conference on Automated Deduction (CADE-13), eds. M. A. McRobbie and J. K. Slaney, Rutgers University, New Brunswick, NJ, USA, July 30-August 3, 1996, Lecture Notes in Artificial Intelligence Vol 1104, Springer-Verlag, pages 201-215.
• A Mechanically Verified Verification Condition Generator. (PDF)

Peter V. Homeier and David F. Martin.
The Computer Journal, Vol. 38, No. 2, July 1995, pages 131-141.
• Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures. (Ph.D. Dissertation)

Peter V. Homeier.
Department of Computer Science, University of California, Los Angeles, June 1995.
• Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator.(PDF)

Peter V. Homeier and David F. Martin.
Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, eds. Thomas Melham and Juanito Camilleri, Valletta, Malta, September 19-22, 1994, Lecture Notes in Computer Science Vol 859, Springer-Verlag, pages 269-284.

 The Machine-Assisted Proof of Programming Language Properties.
Myra VanInwegen
PhD Thesis completed in May of 1996.

Related Sites on HOL

• HOL at Sourceforge
• Introduction to HOL, edited by M. J. C. Gordon and T. F. Melham. This serves excellently both as a tutorial and as a reference.
• Cambridge
• Brigham Young
• Glasgow
• Formal Methods Virtual Library

Conference on Higher Order Logics

The conference will be a venue for presentations on the following topics, among others: advances in interactive theorem proving, proof automation and decision procedures, applications of mechanized theorem proving, comparison between different theorem proving approaches, exploiting external tools within theorem provers and incorporating theorem provers into larger systems.