Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) id <2104-0@swan.cl.cam.ac.uk>; Tue, 16 Jul 1991 01:51:41 +0100 Received: from iris.eecs.ucdavis.edu by ted.cs.uidaho.edu (15.11/1.34) id AA18773; Mon, 15 Jul 91 17:28:51 pdt Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.7.0) id AA27419; Mon, 15 Jul 91 17:31:46 -0700 Date: Mon, 15 Jul 91 17:31:46 -0700 From: schubert@edu.ucdavis.eecs.iris (Tom Schubert) Message-Id: <9107160031.AA27419@iris.eecs.ucdavis.edu> To: info-hol@edu.uidaho.cs.ted Preliminary Program for the 1991 International Workshop on the HOL Theorem Proving System and its Applications Memorial Union Building, University of California, Davis Tuesday, August 27, 1991 A Full-Day Tutorial on: The HOL Theorem-Proving System and its Applications ( see below for more details) Wednesday, August 28, 1991 8:00 - Registration and Continental Breakfast 8:25 - Opening Remarks Myla Archer 8:30 - Day's Keynote Speaker: Kurt Keutzer, Synopsys, Inc. The Need for Formal Verification in Hardware Design and What Formal Verification Has NOT Done for Me Lately 9:15 - Hardware Verification I, Shui-Kai Chin, Syracuse University Representing CCS in HOL with Applications to Verifying Composed Hardware Devices E. T. Schubert, University of California, Davis An HOL Theory for Logic States with Indeterminate Strengths J. W. Gambles and P. J. Windley, University of Idaho COSHOL: Symbolic Circuit Simulation + Higher-Order Logic J. J. Joyce and C. Seger, University of British Columbia 10:30 - Break 10:45 - Hardware Verification II, John Herbert, SRI Cambridge Formalization of VHDL Synthesis Procedures in Higher-Order Logic X. Wang and E. P. Stable, Syracuse University Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic S-K. Chin and G. Birtwistle, Syracuse University and University of Calgary Industrial Applications of Formal Techniques at System Level Design A. Camilleri and R. Fleming, Hewlett-Packard Labs, Bristol 12:00 - Lunch 1:15 - Real-Time and Temporal Issues, Jeff Joyce, University of British Columbia A Formal Method for Hard Real-Time Programming M. Gordon, University of Cambridge Implementing a Real-Time Process Algebra in HOL R. Gerber and E. Gunther, University of Pennsylvania and AT&T Bell Labs Mechanising the Temporal Logic of Actions in HOL (Abstract) J. von Wright, SHH, Finland 2:30 - Proof Systems, Albert Camilleri, HP Labs, Bristol Using HOL to Produce Custom Verification Tools D. Shepherd, INMOS Ltd. Integrating a First-Order Automatic Prover in the HOL Environment K. Schneider, R. Kumar, and T. Kropf, Universitaet Karlsruhe Towards Window Inference in the HOL System J. Grundy, University of Cambridge "A Small Step for Man, but a Giant Leap for Mankind" - First Steps Towards Automating Hardware Proofs in HOL K. Schneider, R. Kumar, and T. Kropf, Universitaet Karlsruhe 4:00 - Break 4:15 - Business Meeting, Myla Archer, General Chair 6:30 - Reception Thursday, August 29, 1991 8:00 - Continental Breakfast 8:30 - Day's Keynote Speaker: John Rushby, SRI International Design Choices in Specification Languages and Verification Systems 9:15 - Panel: Verification in Industry Albert Camilleri, Hewlett-Packard Labs, Bristol Gerald C. Cohen, Boeing Company Cheryl Harkness, Hewlett-Packard Design Technology Center Ken Albin, Rockwell International 10:15 - Break 10:30 - Program Verification, TBD, Mechanizing Program Verification in HOL S. Algerholm, Aarhus University Proof of Program Transformation R. Roxas and M. Newey, Australian National University Program Transformations and Refinements in HOL J. von Wright, SHH, Finland 11:45 - Lunch 1:00 - Verifying Computer Systems, TBD, Case Studies in Compiler Correctness Using HOL D. Martin and R. Toal, University of California, Los Angeles A Verified Compiler for a Structured Assembly Language P. Curzon, University of Cambridge Mechanical Verification of Secure Distributed Systems in Higher Order Logic J. Alves-Foss and K. Levitt, University of Idaho and University of California, Davis 2:15 - Reports on the HOL Theorem Proving System, Mike Gordon, University of Cambridge HOL90: Not Just an Ugly Rumour! K. Slind, University of Calgary A Report on ICL HOL R. D. Arthan, ICL Defense Systems A Report on HOL88 T. F. Melham, University of Cambridge 3:30 - Break 3:45 - Interfaces to HOL, Myla Archer, University of California, Davis Centaur as a Front-End of HOL L. Thery and I. Antipolis, INRIA PM: A Tree-Editor-Based Proof Manager G. Fink and M. Archer, University of California, Davis Building Interfaces to HOL S. Kalvala, University of Cambridge 6:30 - Dinner Satiety Winery Friday, August 30, 1991 8:00 - Continental Breakfast 8:30 - Day's Keynote Speaker: Matt Kaufmann, Computational Logic, Inc. An Informal Discussion of Issues in Mechanically-Assisted Reasoning 9:15 - HOL and Other Theorem Proving Systems, Karl Levitt, University of California, Davis Interactive Synthesis in Higher Order Logic - Abstract S. Finn, M. P. Fourman, and G. Musgrave, Abstract Hardware Ltd. On the Comparison of HOL and Boyer-Moore for Formal Hardware Verification C. M. Angelo, D. Verkest, L. Claesen, and H. De Man, IMEC An Interface Logic for Verification Environments J. D. Guttman, MITRE 10:30 - Break 10:45 - Theories and Packages I, Elsa Gunter, AT&T Bell Labs A Package for Inductive Definitions in HOL T. F. Melham, University of Cambridge Defining Recursive Functions in HOL W. Ploegaerts, L. Claesen, and H. De Man, IMEC Recursive Boolean Functions and their Application in HOL F. Andersen and K.D. Peterson, Telecomms Research Laboratory 12:00 - Lunch 1:15 - Theories and Packages II, Tom Melham, University of Cambridge Proof Based Computation M. Newey, Australian National University Reasoning About Petri Nets in HOL E. Lucena, University of Cambridge A Simple Graph Theory and its Application in Railway Signalling W. Wong, University of Warwick 2:30 - Closing Remarks Myla Archer _________________________________________________________________ A Full-Day Tutorial on: ---------------------- The HOL Theorem-Proving System and its Applications --------------------------------------------------- Tuesday, August 27, 1991 8:30am-5:00pm OVERVIEW This full-day tutorial will be given by a panel of invited HOL experts on a range of topics, including: an overview of the sys- tem, a survey of applications; comparison of HOL with other ve- rification systems; what helps and what hinders new users; the integration of HOL with existing methodologies, tools and en- vironments. WHO WILL BENEFIT This tutorial is designed for an audience not necessarily fami- liar with the HOL system or its applications. It is intended primarily to give prospective users an informed basis for evaluating the HOL system and its potential. This tutorial may also interest those planning to attend the 3-day International Workshop on the HOL Theorem Proving System and its Application, August 28-30 (also in Davis, California). See page 109 of IEEE Computer, May 1991 issue. THE HOL SYSTEM The HOL is an interactive environment for machine-assisted theorem-proving in higher-order logic. This system, developed by researchers at Cambridge University, is currently in use at sites in North America, Europe, Australia, China and Japan. It is used for a number of applications including: + hardware verification + software verification + protocol specification Specialized applications include both safety-critical hardware and computer system security. Users include academic and indus- trial researchers, and companies doing contract proofs. PRELIMINARY PROGRAM Tutorial Overview ----------------- Jeff Joyce, University of British Columbia (Canada) An overview of this 1-day tutorial. Introduction to the HOL System ------------------------------ Mike Gordon, Cambridge University (UK) A very brief look at the HOL system addressing questions such as: what is higher-order logic ? what is ML ? how is the HOL system used ? HOL Aroung the World -------------------- Sara Kalvala, U of California Davis (USA)/Cambridge University (UK) A brief summary of activities involving HOL will be given. The aim is to provide an intuition of the range of possible uses, by experts in a variety of fields --- logicians, hardware designers, softare developers, among others. The motivation behind these ap- plications will be explained, as well as the suitability of the HOL system for each of them. Survey of Hardware Verification in HOL -------------------------------------- Luc Claesen, IMEC/Kath. Univ. Leuven (Belgium) A birds' view on formal hardware verification will be given. The modeling in HOL of hardware at different levels of abstraction is presented and illustrated with some simple examples. Hereafter an overview will be given of the practical experiences in verifying hardware in HOL will be given: TAMARACK microprocessor, safety critical VIPER application, formal proof of UART device, UC Davis "chip set" including AVM-1 microprocessor, proof of arithmetic operators, proof of parameterized hardware modules in CATHEDRAL. Afterwards a comparison of the state of the verification work in the HOL community with the current state in several other systems and approaches will be given. Dealing with Temporal Complexity in Hardware Verification --------------------------------------------------------- John Herbert, SRI International/Cambridge University (UK) This talk will give an overview of modelling and verifying tem- poral aspects of behaviour in HOL. In HOL one can choose to em- ploy a temporal logic or model time explicitly using functions over time. The technique of temporal abstraction will be presented. This can be used to formally relate behaviour at two different levels of time. The problems of dealing with complex timing behaviour will be discussed, and digital hardware examples will illustrate the models and techniques. Abstraction, Recursion and Induction in Hardware Verification ------------------------------------------------------------- Shiu-Kai Chin, Syracuse University (USA) Theorem-based design uses logical inference rather than simula- tion to determine or verify the properties of design implementa- tions. The initial effort to make such an approach practical is large when compared to conventional simulation. However, the cost of this effort is typically incurred only once. The hardware descriptions are parameterized so that the verification results are applicable to an entire set of designs rather than just one instantiation. To illustrate these ideas, we outline the logical structure used to verify arithmetic hardware in HOL. In particular, we show the role of data abstraction, recursion, and induction in this approach. Verifying Microprocessors ------------------------- Phil Windley, University of Idaho (USA) Microprocessor verification is one of the best understood areas of hardware verification. Several microprocessors have been ver- ified and some of these have been implemented. Research contin- ues on increasing the complexity of microprocessors that can be verified. This talk will compare several verified microproces- sors and describe the techniques used to specify and verify mi- croprocessors. We will see that microprocessor verification re- lies on both data and temporal abstraction to manage complexity. Verifying Integrated Systems ---------------------------- Tom Schubert, University of California, Davis (USA) This talk will describe work performed by the Hardware Verifica- tion Group at the University of California, Davis. Our main em- phasis is on the verification of "real" systems. We have veri- fied a CPU, DMA, Floating Point Coprocessor, and a Memory Manage- ment unit. Work is underway to verify a bus controller and an in- terrupt controller. It is hoped that the outcome of this work will be a convincing demonstration of the feasibility of applying verification to a large class of practical systems. In addition, through the examples being verified, we are confronting problems in applying mechanical verification methods to large systems that are suggestive of future research directions. Computer Architecture Specification ----------------------------------- Tim Leonard, Digital Equipment Corporation (USA) Computer architecture specifications are (currently informal) in- terface specifications. I'll talk about some problems with in- formal interface specifications, with a little attention to computer-architecture specifications in particular. Then I'll point out ways in which writing interface specifications (as an end) is different from specifying and verifying implementations. Finally, I'll discuss some of the difficulties and advantages of writing and using formal, rather than informal, specifications in this context. Embedding Formalisms in Higher-Order Logic ------------------------------------------ Jeff Joyce, University of British Columbia (Canada) The ability to semantically embed other formalisms in higher- order logic is an attractive feature of the HOL system. Embed- ding specialized formalisms such as temporal logics can result in more concise specifications and easier proofs. Semantic embed- ding can also be used as a technique for establishing a rigorous link between HOL and specification languages such as CSP (for communicating processes), VHDL, Ella and Silage (for hardware specification). The semantic embedding of a formalism in the HOL system can also be viewed as a convenient mechanism for the rapid prototyping of special-purpose reasoning tools. This talk will briefly explain the advantages of a semantic approach rather than a syntactic approach. I will also briefly survey some of the formalisms which have been embedded in the HOL system. Reasoning about Software ------------------------ Roger Hale, SRI International (UK) The aim of my talk is to get across the idea that HOL is an ap- propriate tool for reasoning about software as well as hardware. Many kinds of programming language semantics (denotational, alge- braic, operational, etc) may be embedded in the HOL logic. Based on these semantics, one can construct tools to support program verification, e.g. using a standard programming logic. Further- more, by modelling the compilation process in the HOL logic, one can verify that a program's meaning (including its timing behaviour) is in fact preserved when it is compiled and run, thus bridging the gap between hardware and software. Reasoning about Communication Protocols --------------------------------------- Rachel Cardell-Oliver, Cambridge University (UK) and DSTO (Aus- tralia) The HOL theorem prover has been used to specify and verify com- munications protocols such as sliding window protocols. The main advantages of using HOL over other formalisms are the ability to: write generic (re-usable) specifications; verify implementations within a hierarchy of more abstract specifications; program proof tools and to build higher level formal methods support onto ex- isting HOL theories. I shall discuss how my work relates to oth- er formal methods for protocol specification and verification, summarise what I have done in HOL, and describe how this work could be extended in order to verify more realistic systems. Reasoning about Computer Security --------------------------------- Karl Levitt, University of California, Davis (USA) Computer security is an important application of verification technology. The talk will present the following: an overview of computer security, emphasizing the formulation of security pro- perties; general techniques for verifying the security of operat- ing system designs, including a survey of security verification systems that use other logics, such as Boyer-Moore and EHDM; and our current work on using HOL to verify the security of distri- buted system designs. The speaker will also discuss the feasi- bility of applying these techniques to real operating systems Future Directions ----------------- Tom Melham, Cambridge University (UK) This talk will summarize some ways in which the HOL system is likely to develop over the next few years. New Interfaces for HOL ---------------------- Laurent Thery, INRIA (France) We present the current state of an interface for HOL running under X. The interest of the interface has been to ease the part of HOL which deals with backward proofs. The demonstration will be composed of a proof of a simple arithmetic theorem using that interface. Learning to Use HOL ------------------- Paul Loewenstein, Mitsubishi Electronics America Inc., (USA) My four years using HOL for verification has taught me much. The initial difficulty of coping with an unfriendly system, through some initial simple examples to more complex examples has gen- erated frustration, enlightenment, boredom and occasional tri- umph. This presentation looks at these experiences and draws con- clusions about what is feasible now, and what needs to be done to make theorem proving a viable verification technique for real systems. Experience with Formal Methods in Industry ------------------------------------------ Albert Camilleri, Hewlett-Packard Laboratories (UK) To establish formal techniques as a routine part of the industri- al design process, whether for software or hardware, is a goal which the formal methods community is yet to achieve. Throughout the past two decades or so, several attempts have been made, but the common belief is still that these techniques have not yet reached the required maturity to enable such a transfer of tech- nology. Indeed this could be considered as slow progress, espe- cially when compared to that made by other computer science tech- nologies. In this paper, the author places particular emphasis on formal verification, and attempts to analyse where the technology really stands at present, what barriers still remain to be bro- ken, and in what form can formal methods by used in industry now to still benefit the design process. _________________________________________________________________ REGISTRATION DETAILS Registration for the full-day tutorial on August 27th is separate from the 3-day workshop which follows the tutorial. Tutorial registration includes lunch and tutorial notes. Early Registration fee for Tutorial, August 27th: Member: $70.00 Non-Member: $90.00 Early Registration fee for Workshop, August 28th - 30th: Member: $280.00 Non-Member: $350.00 Students: $120.00 Early registration will end August 9th. After this date late registration will be accepted as follows: Late Registration fee for Tutorial: Member: $100.00 Non-Member: $125.00 Late Registration fee for Workshop: Member: $340.00 Non-Member: $425.00 Students: $120.00 The Tutorial registration fee covers: Tuesday, August 27th - Tutorial and Tutorial Notes, Continental Breakfast and Lunch The Workshop registration fee covers: Wednesday, August 28th - Workshop, Continental Breakfast, Lunch and Reception Thursday, August 29th - Workshop, Continental Breakfast, Lunch and Banquet at Satiety Winery Friday, August 30th - Workshop, Continental Breakfast and Lunch Registration fees should be paid in U.S. dollars by cash, check or money order made payable to ACM/IEEE HOL '91 Workshop. Hotel Reservations can be made at either of the following motels: Best Western University Lodge Campus Inn 123 "B" st. 221 "D" St. Davis, CA 95616 Davis, CA 95616 (916)756-7890 (916)756-1040 (800)528-1234 FAX (916)753-7287 FAX (916)756-0245 Single and Double rooms will be reserved under the name ACM/IEEE HOL Workshop. Both facilities are within walking distance of the University. You must call or write by August 15th to reserve your room. After this date the rooms are no longer guaranteed. If you are faxing your reservation, please be sure to include the following information: - first and last names - nights of accomodations - how many in your party - kind of accommodations (more than one bed) Also mention that you are affiliated with the ACM/IEEE HOL Workshop. Transportation to and from the Sacramento airport: Davis is reachable from Sacramento Airport as follows: I-5 South to I-80 West to Davis exit. Davis is on I-80 approximately 15 miles West of Sacramento. Taxi $40.00 (approximately) Davis Airporter $18.00/person (Reservations are very helpful: (916) 756-6715) HOL Workshop Van We will do our best to provide transportation to and from the airport for those that need it. The van schedule will be arranged to handle peak arrival/departure times of participants. Typical August Temperatures (in degrees Fahrenheit): Daytime Evening Davis 90-100 60-70 Lake Tahoe 60-80 30-40 San Francisco 65-85 50-60 Please return this page with your payment to Meshell Robinson University of California, Davis Division of Computer Science Davis, CA 95616-8562 (916)752-1974 FAX (916)752-4767 E-mail robinson@cs.ucdavis.edu Name:___________________________________________________________________ ACM/IEEE Membership number:_____________________________________________ Company or University affiliation:______________________________________ Mailing Address:________________________________________________________ ________________________________________________________________________ Telephone:______________ E-mail Address:_________________________ Are you planning to attend the Tutorial on Tuesday, August 27th: yes or no Dates of the Workshop you are planning to attend:_______________________ Would you like to be met by the HOL Workshop van at Sacramento Metro airport: yes or no If requesting HOL van pickup, please list the following information: Arrival airline and flight number:_________________________________ Arrival date and time:_____________________________________________ Departure date and time:___________________________________________ Will you need a local map before you arrive: yes or no Do you plan to make your own Hotel Reservations: yes or no Do you need assistance with your Hotel Reservations: yes or no If you need assistance with Hotel Reservations, please supply the following information: Dates accomodations needed:____________________________________ Single or double occupancy (circle one). If you will be sharing a room with a conference participant, please identify the person so we will avoid making duplicate reservations. (Conference participant's name:________________________________)