[Prev][Next][Index]

Larch Prover Course 17 and 18 March 1994

     The Computer Science department of the University of St. Andrews is
holding an intensive two day course on Larch Prover (LP) on 17th and 18th
March 1994.

     The course will be given by Dr. Steve Garland from MIT and will be
backed up by practical exercises using the prover running on Unix
workstations.

     LP [1] is an interactive proof-assistant for a subset of multisorted
first-order logic.  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 [2], reasoning about concurrent algorithms and hardware designs
[4,5], and proving theorems in algebra [3].

     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.

     LP allows users to axiomatize theories by equations (i.e., quantifier-free
formulas), operator theories (e.g., commutativity), deduction rules (equivalent
to universal-existential formulas), and induction rules.  LP automatically
orients most equations into terminating rewrite rules, which it then uses in
equational term-rewriting to simplify axioms and conjectures.  LP automatically
applies deduction rules to derive consequences from newly asserted, simplified,
or proved equations and rewrite rules.

     If you are interested in attending this course, please contact
Margaret Anderson (margaret@dcs.st-and.ac.uk) +44 334 63251 by Friday, 25th
February 1994. There will be a small charge for attendance to pay for
administration and materials.

References
----------

[1] S. J. Garland and J. V. Guttag.  A Guide to LP, The Larch Prover.  MIT
    Laboratory for Computer Science, December 1991.  Also available from DEC
    Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, as Report
    82.  A PostScript file containing this report is part of the distribution.

[2] S. J. Garland, J. V. Guttag, and J. J. Horning. "Debugging Larch Shared
    Language specifications," IEEE Transactions on Software Engineering 16:9
    (September 1990), pp. 1044-1057.  Also available as DEC Systems Research
    Center Report 60 (July 1990).

[3] U. Martin and M. Lai, "Some experiments with a completion theorem prover,"
    Journal of Symbolic Computation, Journal of Symbolic Computation (1992)
    13, 81-100


[4] J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning, "Using
    transformations and verification in circuit design," DEC Systems Research
    Center Report 78, September 1991.

[5] J. Staunstrup, S. J. Garland, and J. V. Guttag.  "Localized verification of
    circuit descriptions," Proc. Int. Workshop on Automatic Verification
    Methods for Finite State Systems, Grenoble, France, Lecture Notes in
    Computer Science 407, Springer-Verlag, 1989, pp. 349-364.


-----------
Simon Brock,
Computer Science,
University of St.Andrews,                  E-mail: shb@dcs.st-and.ac.uk
North Haugh,                               Tel:    0334 63266
St. Andrews,                                       0334 76161 x3266
Fife KY16 9SS.                             Fax:    0334 63278



%%% overflow headers %%%
To: larch-interest, eas@dcs.rhbnc.ac.uk, Joseph.Goguen@prg.ox.ac.uk,
        muffy@dcs.glasgow.ac.uk, kjt@compsci.stirling.ac.uk, br@inf.rl.ac.uk,
        ajmi@dcs.edinburgh.ac.uk, rb@dcs.edinburgh.ac.uk,
        glc@dcs.edinburgh.ac.uk, Lincoln.Wallen@prg.ox.ac.uk,
        gcs@maths.bath.ac.uk, jhd@maths.bath.ac.uk, Pierre.Lescanne@loria.fr,
        Tobias.Nipkow@Informatik.TU-Muenchen.de, Michael.Rusinowitch@loria.fr,
        Toby.Walsh@loria.fr, cbj@computer-science.manchester.ac.uk,
        jdick@uk03.bull.co.uk
%%% end overflow headers %%%