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
in the
Systems Research
Center in Palo Alto, California. Other currently active sites are listed
below.
MIT Larch Pages
Of Recent Interest
The mailing list larch-interest@pa.dec.com no longer exists. It has been
replaced by the usenet newsgroup
comp.specification.larch, which is intended for discussion of all aspects
of the Larch methdology, languages, and tools. Interesting past messages to
the newsgroup and mailing list are available on the Web in the
larch archive, which now resides at MIT.
Jim Horning has written a paper, ``The Larch Shared
Language: Some Open Problems,'' which has just appeared in Recent Trends
in Data Type Specification, a collection of selected papers from the
11th Workshop on Specification of Abstract Data Types held in Oslo, Norway, in
Sepember 1995. Slides from his talk are
also available.
LCLint detects errors relating to dynamic
memory management: uses of deallocated storage, memory leaks, dangerous
data sharing or unexpected aliasing, uses of possibly undefined storage,
dereferencing a possibly null pointer. See ``Static
Detection of Dynamic Memory Errors'' by David Evans, SIGPLAN
Conference on Programming Language Design and Implementation (PLDI
'96), Philadelphia, PA, May 21-24, 1996.
Larch Sites and Participants
-
MIT Laboratory for Computer Science
(John Guttag,
Steve Garland)
Software Devices and
Systems Group
-
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++ and
Larch/Smalltalk
-
INRIA Lorraine, France
(Pierre Lescanne)
Larch at Nancy
-
Danish Technical University
(Jorgen Staunstrup)
Hardware verification using LP
-
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
Penelope Environment for Mathematics and Ada Verification
-
Rome Laboratory, New York
(Bob Paragi)
Formal Hardware Verification Effort
- University of St. Andrews, Scotland
(Ursula Martin, Steve Linton)
Algebraic Computation group
Related Pages
Last modified on December 10, 1999
Please send suggestions to larch-www@larch.lcs.mit.edu.