Larch Prover

The Larch Prover, or LP for short, was an interactive theorem proving system
for multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990s
to reason about designs for circuits, concurrent algorithms, hardware,
and software. 
Unlike most theorem provers, which attempt to find proofs automatically for
correctly stated conjectures, LP was intended to assist users in finding and correcting flaws in
conjectures—the predominant activity in the early stages of the design process. It worked efficiently
on large problems, had many important user amenities, and could be used by relatively naïve users.
Development.
LP was developed by Stephen Garland and John Guttag at the MIT Laboratory for Computer Science
with assistance from James Horning and James Saxe at the DEC Systems Research Center,
as part of the Larch project on formal specifications.
It extended the REVE 2 equational term rewriting system developed by Pierre Lescanne, Randy Forgaard with assistance from David Detlefs and
Katherine Yelick. It supports proofs by equational term rewriting
(for terms with associative-commutative operators), cases, contradiction, induction, generalization, and specialization.
LP was written in the CLU programming language.
Bibliography.
Pascal André, Annya Romanczuk, Jean-Claude Royer, and Aline Vasconcelos, "Checking the consistency of UML
class diagrams using Larch Prover", "Proceedings of the 2000 International Conference on Rigorous Object-Oriented Methods",
page 1, York, UK, BCS Learning &amp; Development Ltd., Swindon, GBR, January 2000.
Boutheina Chetali, "Formal verification of concurrent programs using the Larch Prover", 
"IEEE Transactions on Software Engineering" 24:1, pages 46–62, January 1998. doi: 10.1109/32.663997.
Manfred Broy, "Experiences with software specification and verification using LP, the Larch proof assistant",
"Formal Methods in System Design" 8:3, pages 221–272, 1996.
Urban Engberg, Peter Grønning, and Leslie Lamport, "Mechanical Verification of Concurrent Systems with TLA",
"Computer-Aided Verification", G. v. Bochmann and D. K. Probst editors, Proceedings of the Fourth International Conference CAV'92),
"Lecture Notes in Computer Science" 663, Springer-Verlag, June 1992, pages 44–55.
Urban Engberg, "Reasoning in the Temporal Logic of Actions", BRICS Dissertation Series DS 96–1,
Department of Computer Science, University of Aarhus, Denmark, August 1996. ISSN 1396-7002.
Stephen J. Garland and John V. Guttag, "Inductive methods for reasoning about abstract data types,"
"Fifteenth Annual ACM Symposium on Principles of Programming Languages", pages 219–228, San Diego, CA, January 1988.
Stephen J. Garland and John V. Guttag, "LP: The Larch Prover," "Ninth International Conference on Automated Deduction"
"Lecture Notes in Computer Science" 310, pages 748–749, Argonne, Illinois, May 1988. Springer-Verlag.
Stephen J. Garland, John V. Guttag, and Jørgen Staunstrup, "Verification of VLSI circuits using LP,"
"The Fusion of Hardware Design and Verification", pages 329–345, Glasgow, Scotland, July 4–6, 1988. IFIP WG 10.2, North Holland.
Stephen J. Garland and John V. Guttag, "An overview of LP, the Larch Prover,"
"Third International Conference on Rewriting Techniques and Applications"
"Lecture Notes in Computer Science" 355, pages 137–151, Chapel Hill, NC, April 1989. Springer-Verlag.
Stephen J. Garland and John V. Guttag, "Using LP to debug specifications,"
"Programming Concepts and Methods", Sea of Galilee, Israel, April 2–5, 1990.
IFIP WG 2.2/2.3, North-Holland.
Stephen J. Garland and John V. Guttag, "A Guide to LP: the Larch Prover",
MIT Laboratory for Computer Science, December 1991.
Also published as Digital Equipment Corporation Systems Research Center Report 82, 1991.
Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch,
"Verifying timing properties of concurrent algorithms,"
"FORTE '94: Seventh International Conference on Formal Description Techniques",
pages 259–273, Berne, Switzerland, October 4–7, 1994. Chapman &amp; Hall.
Ursula Martin and Michael Lai, "Some experiments with a completion theorem prover",
"Journal of Symbolic Computation" 13:1, 1992, pages 81–100, ISSN 0747-7171.
Ursula Martin and Jeannette M. Wing, editors,
"First International Workshop on Larch",
Proceedings of the First International Workshop non Larch, Dedham, Massachusetts, July 13–15 1992,
Workshops in Computing, Springer-Verlag, 1992.
Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli, and Nancy Lynch,
Using simulated execution in verifying distributed algorithms,"
"Software Tools for Technology Transfer" 6:1, Lenore D. Zuck, Paul C. Attie,
Agostino Cortesi, and Supratik Mukhopadhyay (editors), pages 67–76. Springer-Verlag, July 2004.
Tsvetomir P. Petrov, Anya Pogosyants, Stephen J. Garland, Victor Luchangco, and Nancy A. Lynch,
"Computer-assisted verification of an algorithm for concurrent timestamps,"
"Formal Description Techniques IX: Theory, Application, and Tools (FORTE/PSTV)",
Reinhard Gotzhein and Jan Bredereke (editors), pages 29–44, Kaiserslautern, Germany, October 8–11, 1996. Chapman &amp; Hall.
James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning,
"Using transformations and verification in circuit design,"
"Formal Methods in System Design" 3:3 (December 1993), pages 181–209.
Jørgen F. Søgaard-Anderson, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anya Pogosyants,
"Computed-assisted simulation proofs," "Fifth Conference on Computer-Aided Verification (CAV '03)",
Costas Courcoubetis (editor), "Lecture Notes in Computer Science" 697, pages 305–319, Elounda, Greece, June 1993. Springer-Verlag.
Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag,
"Localized verification of circuit descriptions,"
"Automatic Verification Methods for Finite State Systems", "Lecture Notes in Computer Science" 407,
pages 349–364, Grenoble, France, June 1989. Springer-Verlag.
Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag,
"Mechanized verification of circuit descriptions using the Larch Prover",
"Theorem Provers in Circuit Design", Victoria Stavridou, Thomas F. Melham, and Raymond T. Boute (editors),
"IFIP Transactions A-10", pages 277–299, Nijmegen, The Netherlands, June 22–24, 1992. North-Holland.
Mark T. Vandevoorde and Deepak Kapur, "Distributed Larch Prover (DLP): an experiment in parallelizing a rewrite-rule based prover",
"International Conference on Rewriting Techniques and Applications RTA 1996",
"Lecture Notes in Computer Science" 1103, pages 420–423. Springer-Verlag.
Frédéric Voisin, "A new proof manager and graphic interface for the Larch prover",
"International Conference on Rewriting Techniques and Applications RTA 1996",
"Lecture Notes in Computer Science" 1103, pages 408–411. Springer-Verlag.
Jeannette M. Wing and Chun Gong, Experience with the Larch Prover,
"ACM SIGSOFT Software Engineering Notes" 15:44, September 1990,
pages 140–143 https://doi.org/10.1145/99571.99835