Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
To: Chris Toshok <toshok@cs.uidaho.edu>
Cc: info-hol@cs.uidaho.edu
Subject: Re: Specification languages in HOL
In-Reply-To: Your message of "Mon, 25 Oct 93 12:52:01 MST." <199310251952.AA09466@panther.cs.uidaho.edu>
Date: Tue, 26 Oct 93 11:40:09 +0000
From: Jim Grundy <Jim.Grundy@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:027290:931026114023"@cl.cam.ac.uk>


Hi

> I am looking specifically for references or information on verifying code by
> way of a semantic description and a specification.

What follows are the references I have to program verification and refinement
work that uses HOL.   In each case the work describes methods of using 
a semantic description to prove that a program meets a specification.   In 
some cases this is done after the program is written, and in other cases
the method describes how to develop the program and the proof in tandem.

Hope this helps

Jim

@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}

@TECHREPORT{Bac89a,
    author      = "Ralph-Johan R. Back and Joakim von Wright",
    title       = "Refinement Concepts Formalized in Higher-Order Logic",
    institution = "Institutionen f{\"{o}}r Informationsbehandling \&
                   Mathematiska Institutet,
                   {\AA}bo Akademi",
    address     = "Lemmink{\"{a}}inengatan 14, SF-20520 Turku, Finland",
    year        = 1989,
    month       = sep,
    number      = "Series A---85",
    type        = "Reports on Computer Science {\&} Mathematics"}

@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{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, Berlin",
    address     = "Banff, Canada"}

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

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

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