Table of contents

  1. Front Matter
  2. Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson
    Pages 1-15
  3. Kim Dam Petersen
    Pages 16-28
  4. Cui Zhang, Rob Shaw, Ronald A. Olsson, Karl Levitt, Myla Archer, Mark R. Heckman et al.
    Pages 29-42
  5. Myra Vanlnwegen, Elsa Gunter
    Pages 61-74
  6. K. G. W. Goossens
    Pages 75-88
  7. Catia M. Angelo, Luc Claesen, Hugo De Man
    Pages 89-100
  8. Dirk Eisenbiegler, Klaus Schneider, Ramayya Kumar
    Pages 101-114
  9. David Lorge Parnas
    Pages 155-162
  10. John Rushby, Mandayam Srivas
    Pages 163-173
  11. Juin-Yeu Lu, Shiu-Kai Chin
    Pages 199-212
  12. Klaus Schneider, Ramayya Kumar, Thomas Kropf
    Pages 213-226
  13. Anthony McIsaac
    Pages 227-238
  14. Tej Arora, Tony Leung, Karl Levitt, Thomas Schubert, Phillip Windley
    Pages 239-252

About these proceedings


This volume constitutes the refereed proceedings of the 1993 Higher-Order Logic User's Group Workshop, held at the University of British Columbia in August 1993. The workshop was sponsored by the Centre for Integrated Computer System Research. It was the sixth in the series of annual international workshops dedicated to the topic of Higher-Order Logic theorem proving, its usage in the HOL system, and its applications. The volume contains 40 papers, including an invited paper by David Parnas, McMaster University, Canada, entitled "Some theorems we should prove".


Automatisches Beweisen Hardwareverifikation Higher Order Logic System (HOL) Higher-Order-Logic System Protocol Verification Protokollverifikation Softwareverifikation Syntax Theorem Proving hardware verification logic modeling processor programming language semantics

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag 1994
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-57826-0
  • Online ISBN 978-3-540-48346-5
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • About this book
Industry Sectors