David Evans,
``Static detection of dynamic memory errors,''
SIGPLAN Conference on Programming Language Design and Implementation,
PLDI '96, Philadelphia, PA, May 21-24, 1996.
(abstract,
paper)
David Evans,
John V. Guttag,
James J. Horning, and
Yang Meng Tan,
``LCLint: a tool for using specifications to check code,''
Symposium on the Foundations of Software Engineering,
December 1994.
(abstract,
paper)
Stephen J. Garland
and
John V. Guttag,
A Guide to LP, the Larch Prover,
MIT Laboratory for Computer Science, December 1991.
Also available as Digital Equipment Corporation Systems Research Center
Research Report 82.
(abstract,
paper)
Stephen J. Garland
and
John V. Guttag,
LP, the Larch Prover: Version 3.1,
MIT Laboratory for Computer Science, January 1995.
(html)
Stephen J. Garland,
John V. Guttag, and
James J. Horning,
``An overview of Larch,''
Functional Programming, Concurrency, Simulation and Automated Reasoning,
Peter E. Lauer (editor),
Springer-Verlag Lecture Notes in Computer Science, Vol. 693, July 1993,
pages 329-348.
(abstract,
paper)
John V. Guttag,
``Goldilocks and the three specifications,''
Fourth International Joint Conference on the Theory and Practice of
Software Development,
Springer-Verlag, 1993.
John V. Guttag and
James J. Horning (editors),
with
Stephen J. Garland,
Kevin D. Jones,
Andrés Modet, and
Jeannette M. Wing,
Larch: Languages and Tools for Formal Specification,
Springer-Verlag Texts and Monographs in Computer Science, 1993,
ISBN 0-387-94006-5, ISBN 3-540-94006-5.
Victor Luchangco,
Ekrem Söylemez,
Stephen J. Garland,
and
Nancy A. Lynch,
``Verifying timing properties of concurrent algorithms,''
FORTE'94: Seventh International Conference on Formal Description
Techniques for Distributed Systems and Communications
Protocols,
Berne, Switzerland, October 4-7, 1994, Chapman and Hall, pages 259-273.
(abstract)
Ursula Martin and
Jeannette M. Wing (editors),
First International Workshop on Larch,
Springer-Verlag, 1992, ISBN 0-387-19804-0, ISBN 0-540-19804-0.
Tsvetomir P. Petrov,
Anna Pogosyants,
Stephen J. Garland,
Victor Luchangco, and
Nancy A. Lynch,
``Computer-assisted verification of an algorithm for concurrent
timestamps,''
Formal Description Techniques IX: Theory, Applications, and Tools,
Reinhard Gotzhein and Jan Bredereke, editors,
Chapman and Hall, 1996, pages 29-44.
(Proceedings of the FORTE/PSTV '96 Joint International Conference on Formal
Description Techniques for Distributed Systems and Communication Protocols, and
Protocol Specification, Testing, and Verification, Kaiserslautern,
Germany, October 8-11, 1996.)
(abstract,
paper)
James B. Saxe,
John V. Guttag,
James J. Horning,
and
Stephen J. Garland,
``Using transformations and verification in circuit design,''
Formal Methods in System Design Vol. 3, No. 3, December 1993,
pages 181-209.
Also available as Digital Equipment Corporation Systems Research Center
Research Report 78.
Ekrem Söylemez,
Automatic Verification of the Timing Properties of MMT Automata,
SM Thesis, MIT Department of Electrical Engineering and Computer Science,
February 1994.
Jørgen F. Søgaard-Anderson,
Stephen J. Garland,
John V. Guttag,
Nancy A. Lynch, and
Anna Pogosyants,
``Computed-assisted simulation proofs,''
Fifth Conference on Computer-Aided Verification,
Costas Courcoubetis (editor),
Crete, June 1993.
Springer-Verlag Lecture Notes in Computer Science 697, pages 305-319.
(abstract)
Raymond Paul Stata
Modularity in the Presence of Subclassing,
Ph. D. Thesis, MIT Department of Electrical Engineering and Computer Science,
June 1996.
Raymie Stata and
John V. Guttag,
"Modular reasoning in the presence of subclassing,"
Object-Oriented Programming Systems, Languages and Appplications 1995,
October 1995.
Jørgen S. Staunstrup,
Stephen J. Garland,
and
John V. Guttag,
``Mechanized verification of circuit descriptions using the Larch Prover,''
Theorem Provers in Circuit Design,
Nijmegen, June 1992.
North-Holland IFIP Transactions A-10, pages 277-299.
(abstract)
Yang Meng Tan,
Formal Specification Techniques for Promoting Software Modularity, Enhancing
Documentation, and Testing Specifications,
Ph. D. Thesis, MIT/LCS/TR-619, June 1994.
(abstract,
paper)
Yang Meng Tan,
``Interface language for supporting programming styles,''
Proceedings of a POPL Workshop on Interface Definition Languages,
Portland, Oregon, January 1994.
Yang Meng Tan,
Formal Specification Techniques for Engineering Modular C,
Kluwer International Series in Software Engineering, Volume 1, Kluwer Academic
Publishers, Boston, 1995.
Mark T. Vandevoorde,
``Specifications can make programs run faster,''
Proceedings of TAPSOFT '93,
Springer Verlag, April 1993.
Mark T. Vandevoorde,
Exploiting Specifications to Improve Program Performance,
Ph. D. Thesis, Technical Report MIT/LCS/TR-598, February 1994.
(abstract,
paper)
Mark T. Vandevoorde and
John V. Guttag,
``Using specialized procedures and specification-based analysis to reduce the
runtime costs of modularity,''
Symposium on the Foundations of Software Engineering,
December 1994.
Mark T. Vandevoorde and
Deepak Kapur,
``Distributed Larch Prover (DLP): an experiment in parallelizing a rewrite-rule
based prover,''
Conference on Rewriting Techniques and Applications,
July 1996.