Larch Home Page
Larch is a multi-site project exploring methods, languages, and tools for the
practical use of formal specifications. Much of the early work was done at MIT in the former Systematic Program Development
Group in the Laboratory for Computer
Science and at Digital
Equipment (now part of Compaq) in its Systems Research
Center in Palo Alto, California. Other Larch sites are listed below.
MIT Larch Pages
Work connected with Larch continues at MIT, but at a lesser level than in the
past. Information about current and past activities can be found on the
following pages.
- Publications from MIT [Outdated]
- A brief description and
history of Larch [Outdated]
- Larch Bibliography (postscript,
TeX source,
bibtex) [Outdated]
- Larch: Languages and Tools for Formal
Specification, John V. Guttag and James J. Horning, editors,
Springer-Verlag, 1993. [Out of print]
- Larch Shared Language Handbook
[Original version, superseded by the version in the current LSL
distribution]
- Tools (in the Larch
distribution directory)
- LP, the Larch Prover
[Maintained, but not under active development]
- LSL, a checker for the Larch Shared
Language [To be replaced by a new version in 2001]
- LCLint, a C program
checker that exploits (and also checks) any accompanying LCL
specifications [Now maintained at the University of
Virginia]
Other Sources of Information
- The comp.specification.larch
discussion group, covering all aspects of the Larch methdology, languages,
and tools.
- A list of Frequently
Asked Questions about Larch, maintained by Gary Leavens at Iowa State.
- Email announcements of new releases of LCLint (send email to
majordomo@virginia.edu
containing subscribe lclint-announce as the body of the message).
- The LCLint discussion group (send email to
majordomo@virginia.edu
containing subscribe lclint-interest as the body of the message).
Larch Sites and Participants
- MIT Laboratory for Computer Science
(Steve Garland,
John Guttag)
Networks and Mobile Systems Group
- InterTrust Star Lab
(Jim Horning)
Jim Horning's Larch
Page
- Digital Equipment Systems Research Center
DEC SRC
Larch Project [Inactive]
- Carnegie Mellon University
(Jeannette
Wing)
CMU
Larch Home Page
- Department of Computer Science, Iowa State University
(Gary T.
Leavens)
Larch/C++,
Larch/Smalltalk
- Department of Computer Science, University of Virginia
(David Evans)
LCLint
- University of St. Andrews, Scotland
(Ursula Martin,
Steve Linton)
Computer
Algebra and Automated Reasoning
- École Normale Supérieure de Lyon, France
(Pierre Lescanne)
- Aarhus University, Denmark
(Urban Engberg)
TLP (The TLA
Proof Checker)
- University of Cincinnati, Ohio
Knowledge-Based Software Engineering Lab
VSPEC, a Larch interface language for VHDL
- Odyssey Research Associates, Ithaca, New York
(David Guaspari, Mark Bickford)
Larch/VHDL;
Penelope,
an Environment for Mathematics and Ada Verification
- Danish Technical University
(Jorgen Staunstrup) [Inactive]
Synchronized Transitions; Hardware verification using LP
- Rome Laboratory, New York
(Bob Paragi)
Formal Hardware Verification
Related Pages
Last modified on January 11, 2001