MIT/LCS Publications about Larch

MIT/LCS Software Devices and Systems Group

David Evans,
Using Specifications to Check Source Code,
SM Thesis, MIT/LCS/TR-628, June 1994.
(abstract, paper)

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.