[Prev][Next][Index][Thread]
Short Course at UBC: Cambridge HOL System
Date: 2 Apr 90 17:17 -0700
The Cambridge HOL System:
========================
An Introduction to Interactive Machine-Assisted
Theorem-Proving in Higher-Order Logic
Monday-Friday, June 4-8, 1990
FIVE-DAY INTENSIVE COURSE
Seminars and Lab Workshops to be held on
The University of British Columbia Campus
(Vancouver Canada)
Sponsored by: The UBC Centre for Continuing Education and
The UBC Centre for Integrated Computer Systems Research
Course Description:
-------------------
This five-day course is an introduction to higher-order logic and use of
the Cambridge HOL System. The HOL system is an interactive environment
for machine-assisted theorem-proving in higher-order logic. This system
is currently in use at sites in North America, Europe, China and Japan.
It is used for hardware verification, software verification and basic
research into machine-assisted formal proof. Users include both companies
doing contract proofs and researchers.
This course will be of particular interest to contractors developing
hardware/software systems to meet increasingly tough standards such as
the UK MoD Interim Defence Standard 00-55 for the development of safety-
critical software and the US DoD Trusted Computer Systems A1 security
classification (both requiring the use of formal verification techniques).
Morning lectures will describe the HOL formulation of higher-order logic
along with some examples of using higher-order logic to specify digital
hardware.
Afternoon laboratory sessions will provide instruction on using the HOL
system to create formal specifications and generate formal proofs.
Course participants will have workstation access to the HOL system for
course exercises.
For more details on using the HOL system to verify digital hardware, see
"The Notion of Proof in Hardware Verification" (by Avra Cohn, Journal of
Automated Reasoning, Vol. 5, May 1989, pp. 127-139) which gives an account
of using the HOL system to partially verify the commercially-available
VIPER microprocessor.
Course Instructors:
-------------------
Rachel Cardell-Oliver, Ph.D. Candidate, Cambridge University/Australian
Defence Science and Technology Organization, (Protocol Specification
and Verification).
John Herbert, Research Associate, Cambridge University/SRI Cambridge,
(Specification and Verification of digital hardware).
Jeff Joyce, Assistant Professor, University of British Columbia,
(Specification and Verification of microprocessor-based systems).
Who will benefit:
-----------------
This course will benefit researchers in both industrial and academic
settings with an interest in the development of reliable hardware/software
systems. A background in formal logic is NOT required, however, some
familiarity with the notation of predicate calculus would be helpful.
Experience with the use of an interactive functional programming language
(such as Lisp) would be very helpful.
Other Information:
------------------
The Cambridge HOL system is available as a public domain system. Copies
of the system will be available at the course (at cost for magnetic tape).
Pre-ordered copies of the three-volume HOL System Manual will also be
available (at cost for copying).
For further course information contact:
Jeff Joyce
Computer Science Department Telephone: (604) 228-4327
The University of British Columbia Fax: (604) 228-5485
6356 Agricultural Road Email: joyce@cs.ubc.ca
Vancouver, B.C. V6T 1W5
Canada
For information regarding registration contact:
Vicki Ayerbe
Computer Science Programs Telephone: (604) 222-5251
Centre for Continuing Education Fax: (604) 222-5283
5997 Iona Drive
Vancouver, B.C. V6T 2A4
Canada
Registration Information:
-------------------------
Course Location: University of British Columbia Campus,
Vancouver, B.C., Canada
Pre-registration deadline: May 7, 1990
Enrollment limited.
Before May 7 After May 7
------------ -----------
Registration Fees: Regular $295.00 $345.00
Student $150.00 $175.00
Also available by order: Software (magnetic tape): $25.00*
Three Volume Manual: $110.00*
* - public domain (copying costs only)
Ways to Register !
Mail your cheque (payable to UBC) along with yhour registration form
(attached below).
In Canada only: Use your VISA or MASTERCARD and register by telephone,
(604) 222-5251, or by FAX at (604) 222-5283, 10am - 4pm, Monday-Friday.
Cancellation Policy: Notice of participant cancellation must be in
writing and must be received by the Centre for Continuing Education
two weeks prior to the course starting date to qualify for a refund
(a full refund less $50.00 cancellation fee). No refund will be
made for cancellation received after that time. The course may
be cancelled by May 14 due to insufficient registrations.
-------------------- CUT HERE --------------------------------------
Accommodation Information and Registration Form
-----------------------------------------------
Walter Gage Residence
Single bedrooms are arranged apartment style (each apartment contains
six private bedrooms with a single bed) with one large shared washroom,
a lounge area with refrigerator and a balcony.
Accommodation payment is requested upon check-in by cash, traveller's
cheque, VISA or MASTERCARD.
NAME: ____________________________________________________
ADDRESS: ____________________________________________________
____________________________________________________
TELEPHONE: ____________________________________________________
ARRIVAL DATE: __________________ DEPARTURE DATE: _________________
Check-in time: 1400 hours (2 pm) Check-out time: 1100 hours (11 am)
Accommodation:
Single Bedroom (sharing washroom and lounge) $28.00/night
A deposit is not required.
A provincial hotel tax, currently 8%, is added to the above rate.
Send this reservation request form to:
UBC Conference Centre
5961 Student Union Mall
Vancouver, B.C., V6T 2C9 Canada
Telephone: (604) 228-2963
Fax: (604) 228-5297
G00602A
-------------------- CUT HERE --------------------------------------
Course Registration Form
------------------------
The Cambridge HOL System CS 5012-290
____________________________________________________________________
LAST NAME FIRST NAME
____________________________________________________________________
ADDRESS CITY/TOWN
Registration Fee: $______________
Software (optional): $______________
Manual (optional): $______________
TOTAL: $______________
Method of Payment
Cheque/Money Order (Payable to UBC)
Cash (For Registration in person)
VISA Card __________________________
MASTERCARD _________________________
Valid Date: ______________ Expiry Date: ______________
(if MASTERCARD)
I authorize UBC to charge the above amount to my credit card
Signature _____________________________________________________
Name of person paying for program (s) (if different than registrant)
Mail completed registration form to:
REGISTRATIONS,
CENTRE FOR CONTINUING EDUCATION,
THE UNIVERISTY OF BRITISH COLUMBIA
5997 IONA DRIVE,
VANCOUVER, B.C., V6T 2A4
CANADA