Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Wed, 15 Jun 1994 11:54:00 +0930
From: Jim Grundy <jug@itd.dsto.gov.au>
Message-Id: <9406150224.AA16804@itd0.dsto.gov.au>
To: mel@ultrastar.EE.CORNELL.EDU
Subject: Re: Information on uses of HOL for software verification
In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Tue, 14 Jun 94 16:49:40 EDT
Cc: info-hol@cs.uidaho.edu

Hi

Miriam Leeser writes:
> I am looking for information about uses of HOL for reasonably sized
> software verification efforts.  A case study of HOL used to verify
> software that is part of an actual software system is the kind of thing I
> am looking for.  Any citations would be greatly appreciated.
> 
> Also, does anyone know of a good reference that discusses advantages
> of higher-order logic theorem provers over first-order logic theorem
> provers?

I have included below some entries from my bibtex files that I think may
be usefull to you.   The majority are related to efforts to develope 
verified software.  Unfortunately I don't think any of them actually
describe what you are looking for (the construction of a nontrivial,
real-world, verified application using HOL, I'm not sure that such a beast
exists, please let me know if you find one).

Jim Grundy

@MASTERSTHESIS{Age92a,
    author      = "Sten Agerholm",
    title       = "Mechanizing Program Verification in {HOL}",
    school      = "Computer Science Department, Matematisk Institut,
		    {\AA}rhus Universitet",
    address     = "Ny Munkegade, Building 540, DK-8000 {\AA}rhus C,
		    Denmark",
    year        = 1992,
    month       = apr}

@ARTICLE{Bac90a,
    author      = "Ralph-Johan R. Back and Joakim von Wright",
    title       = "Refinement Concepts Formalised in Higher-Order Logic",
    journal     = "Formal Aspects of Computing",
    year        = 1990,
    volume      = 2,
    number      = 3,
    month       = jul,
    pages       = "247--272"}

@INPROCEEDINGS{Bac92b,
    author      = "Ralph-Johan R. Back and Joakim von Wright",
    title       = "Predicate Transformers and Higher Order Logic",
    pages       = "1--20",
    editor      = "J. W. de Bakker and Willem-Paul de Roever and G. Rozenberg",
    booktitle   = "Semantics: Foundations and Applications ---
                    Proceedings of the {REX} Workshop",
    series      = "Lecture Notes in Computer Science",
    volume      = 666,
    address     = "Beekbergen, The Netherlands",
    month       = "1--4 " # jun,
    year        = 1992,
    publisher   = "Springer-Verlag"}

@INPROCEEDINGS{Gor85a,
    author      = "Michael J. C. Gordon",
    title       = "Why Higher-Order Logic is a Good Formalism for
                    Specifying and Verifying Hardware",
    booktitle   = "Proceedings of the 1985 Edinburgh Workshop on {VLSI} Design:
                    Formal Aspects of {VLSI} Design",
    editor      = "George J. Milne and P. A. Subrahmanyam",
    address     = "Edinburgh, Scotland",
    year        = 1985,
    publisher   = "North Holland",
    pages       = "153--177"}

@INPROCEEDINGS{Gor88a,
    author      = "Michael J. C. Gordon",
    title       = "Mechanizing Programming Logics in Higher-Order Logic",
    booktitle   = "Current Trends in Hardware Verification and
                    Automated Theorem Proving
                    ({P}roceedings of the Workshop on Hardware Verification)",
    editor      = "Graham M. Birtwistle and P. A. Subrahmanyam",
    chapter     = 10,
    year        = 1988,
    pages       = "387--439",
    publisher   = "Springer-Verlag",
    address     = "Banff, Canada"}

@INPROCEEDINGS{Gru92a,
    author      = "Jim Grundy",
    title       = "A Window Inference Tool for Refinement",
    pages       = "230--254",
    editor      = "Cliff B. Jones and B. Tim Denvir and Roger C. F. Shaw",
    booktitle   = "Proceedings of the 5th Refinement Workshop",
    series      = "Workshops in Computing",
    address     = "Lloyd's Register, London",
    month       = "8--10 " # jan,
    year        = 1992,
    organization= "BCS-FACS",
    publisher   = "Springer-Verlag"}

@PHDTHESIS{Gru93c,
    author      = "Jim Grundy",
    title       = "A Method of Program Refinement",
    school      = "University of Cambridge, Computer Laboratory",
    address     = "New Museums Site, Pembroke Street, Cambridge CB2 3QG,
		    England",
    month       = nov,
    year        = 1993}

@INPROCEEDINGS{Joy91a,
    author      = "Jeffrey J. Joyce",
    title       = "More Reasons Why Higher-Order Logic is a Good Formalism
                    for Specifying and Verifying Hardware",
    booktitle   = "Proceedings of the 1991 International Workshop on Formal
                    Methods in {VLSI} Design",
    editor      = "P. A. Subrahmanyam",
    year        = 1991,
    month       = jan,
    address     = "Miami",
    organisation= "ACM-SIGDA / IFIP WG 10.2",
    publisher   = "Springer-Verlag"}

@ARTICLE{Tre92a,
    author      = "Gavan Tredoux",
    title       = "Mechanizing Execution Sequence Semantics in {HOL}",
    journal     = "The South African Computer Journal",
    volume      = 7,
    month       = jul,
    year        = 1992}

@INPROCEEDINGS{Wri91a,
    author      = "Joakim von Wright and K. Sere",
    title       = "Program Transformations and Refinements in {HOL}",
    pages       = "231--239",
    editor      = "Phillip J. Windley and Myla Archer and Karl N. Levitt and
                    Jeffrey J. Joyce",
    booktitle   = "Proceedings of the
                    International Tutorial and Workshop on the
                    {HOL} Theorem Proving System and its Applications",
    address     = "University of California at Davis",
    month       = "28--30 " # aug,
    year        = 1991,
    organization= "ACM-SIGDA / IEEE Computer Society",
    publisher   = "IEEE Computer Society Press"}

@ARTICLE{Wri93a,
    author      = "Joakim von Wright and J. Hekanaho and P. Loustarinen and
                    Thomas L{\aa}ngbaka",
    title       = "Mechanising Some Advanced Refinement Concepts",
    journal     = "Formal Methods in System Design",
    volume      = 3,
    number      = "1/2",
    month       = aug,
    year        = 1993}

@INPROCEEDINGS{Wri94a,
    author      = "Joakim von Wright",
    title       = "Program Refinement by Theorem Prover",
    editor      = "David Till and Roger C. F. Shaw",
    booktitle   = "Proceedings of the 6th Refinement Workshop",
    series      = "Workshops in Computing",
    address     = "City University, London",
    month       = "5--7 " # jan,
    year        = 1994,
    organization= "BCS-FACS",
    publisher   = "Springer-Verlag"}