[Prev][Next][Index]

LARCH THEOREM PROVER COURSE





                                UNIVERSITY OF ST ANDREWS

                                COMPUTER SCIENCE DIVISION

                               LARCH THEOREM PROVER COURSE

                               PROFESSOR STEVE GARLAND, MIT

                                     17-18 March 1994


LARCH PROVER

The Larch Prover LP is an interactive proof-assistant for a subset of
multisorted first-order logic. It has been developed by Steve Garland and
John Guttag at MIT, in collaboration with DEC-SRC. It is designed to work
efficiently on large problems and to be used by relatively naive users.
Among its current uses are analyzing formal specifications, modelling
safety-critical applications
in LOTOS, reasoning about concurrent algorithms and hardware designs, and
proving theorems in algebra.

LP's design is based on the assumption that initial attempts to state
conjectures correctly, and then prove them, usually fail. As a result, LP
is designed to carry out routine (and possibly lengthy) steps in a proof
automatically and to provide useful information about why proofs fail, if
and when they do. LP is not designed
to find difficult proofs automatically; instead, LP makes it easy for users
to employ standard techniques such as proofs by cases, induction, and
contradiction.

THIS COURSE

An intensive 2-day tutorial on LP, consisting of lectures and hands-on
practical sessions, will be given in the Computer Science Department of the
University of St Andrews by Dr Steve Garland on 17/18 March.

BACKGROUND KNOWLEDGE

The course will not assume detailed knowledge of any particular
specification or verification technique but attendees should have some
knowledge of specification techniques and how automated reasoning may be
used to support them.

BACKGROUND READING

J V Guttag and J J Horning, Larch: languages and tools for formal
specification, Springer Verlag 1993

U Martin and J M Wing (editors), Proceedings of the First International
Workshop on Larch, Springer Verlag Workshops in Computing Series, 1993

M Thomas, A proof of incorrectness using the the LP theorem prover: the
editing problem in the Therac-25, High Integrity Systems Journal 1, 1993

-------------------------------------------------------------------------------

TO REGISTER, please apply using the form/template below.  Completed forms
should be returned to me by Wednesday 9 March, by email, post or fax.

POSTAL REGISTRATIONS with cheques made payable to "University of St Andrews"
should be sent to:

Miss Margaret Anderson, Computer Science Division,
University of St Andrews, North Haugh, St Andrews, Fife, KY16 9SS, UK

We will accept payment at the workshop, with prior agreement.

The registration fee includes all materials.

The course dinner, which is extra, is on Thursday 17 March.

There are several hotels and guest houses offering bed and breakfast. Prices
range from as little as 15 pounds, up to 75 pounds, per person per night.

Anyone requiring information about accommodation should contact me by email
or phone.

Email:  margaret@dcs.st-and.ac.uk
Phone:  +44 334 63251
Fax:    +44 334 63278




PLEASE COMPLETE A SEPARATE COPY OF THE FORM/TEMPLATE FOR EACH PARTICIPANT.

===========================================================================

          LARCH THEOREM PROVER COURSE REGISTRATION FORM/TEMPLATE
          ------------------------------------------------------


                                                Academic           Industrial

REGISTRATION:                                   100 [  ]           150 [  ]


CONFERENCE DINNER                                25 [  ]            25 [  ]



Name_________________________________________

Organisation_________________________________

Address______________________________________

_____________________________________________

_____________________________________________

E-mail_______________________________

Tel______________________________

==============================================================================

Special dietary needs:
Other special needs:

Arrival date____________  Departure Date____________

I will be travelling by AIR/TRAIN/CAR      _________

=======================================================================