% Larch bibliography
% Last updated by Stephen J. Garland on October 22, 1996

@InCollection(	Baugh92,
       Author = {Baugh, Jr., John~W.},
        Title = {Formal Specification of Engineering Analysis Programs},
    BookTitle = {Expert Systems for Numerical Computing},
       Editor = {Houstis, E.~N. and Rice, J.~R and Vichnevetsky, R.},
    Publisher = {North-Holland},
         Year = 1992
)

@InProceedings(	Baugh92a,
       Author = {Baugh, Jr., John~W.},
        Title = {Is Engineering Software Amenable to Formal Specification?},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@TechReport(	Baugh89,
       Author = {Baugh, Jr., John W. and Rehak, D.~R.},
        Title = {Computational Abstractions for Finite Element Programming},
  Institution = {Department of Civil Engineering, Carnegie Mellon University},
         Type = {TR},
       Number = {89--182},
        Month = {September},
         Year = 1989
)

@InProceedings(	Bidoit92,
       Author = {Bidoit, Michel and Hennicker, Rolf},
        Title = {How to Prove Observational Theorems with {LP}},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992,
)

@Article(	Birrell87,
       Author = {Birrell, Andrew~D. and Guttag, John~V. and Horning, James~J.
                 and Levin, Roy},
        Title = {Synchronization Primitives for a Multiprocessor: A Formal 
                 Specification},
      Journal = {Operating Systems Review},
       Volume = 21,
       Number = 5,
        Month = {November},
         Year = 1987,
         Note = {Also published as DEC Systems Research Center Report 20, 
		 August 1987.  Revised version in \cite{Nelson91}}
)

@InProceedings(	Bourdeau92,
       Author = {Bourdeau, Robert~H. and Cheng, Betty~H.~C.},
	Title = {An Object-oriented Toolkit for Constructing Specification 
		 Editors},
    Booktitle = {COMPSAC'92: Computer Software and Applications Conference},
	Month = {September},
	 Year = 1992
)

@TechReport(	Broy92,
       Author = {Broy, Manfred},
        Title = {Experiences with Software Specification and Verification 
      		  Using {LP}, the {L}arch {P}roof {A}ssistant},
         Type = {Report},
       Number = 93,
  Institution = {DEC Systems Research Center},
      Address = {Palo Alto, CA},
        Month = {October},
         Year = 1992
)

@Article(	Burton89,
       Author = {Burton, C.~T. and Cook, S.~J. and Gikas, S. and Rowson, J.~R.
                 and Sommerville, S.~T.},
        Title = {Specifying the {A}pple {M}acintosh Toolbox Event Manager},
      Journal = {Formal Aspects of Computing},
       Volume = 1,
       Number = 2,
         Year = 1989,
	Pages = {147--171}
)

@InProceedings(	Buth92,
       Author = {Buth, Karl-Heinz},
        Title = {Using {SOS} Definitions in Term-Rewriting Proofs},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@TechReport(	Cardenas88,
       Author = {Cardenas, S.~R. and Oktaba, H.},
        Title = {Formal Specification in {L}arch Case Study: Text Manager.
		 {I}nterface Specification, Implementation, in {A}da and 
		 Validation of Implementation},
  Institution = {Instituto de Investigaciones en Matematicas Aplicadas y en 
		 Sistemas, Universidad Nacional Autonoma de Mexico},
         Type = {TR},
       Number = 511,
         Year = 1988
)

@Unpublished(	Chen89,
       Author = {Chen, Jolly},
        Title = {The {L}arch/{G}eneric Interface Language},
         Year = 1989,
         Note = {S.~B. Thesis, Department of Electrical Engineering and 
                 Computer Science, MIT}
)

@MastersThesis(	Cheon91,
       Author = {Cheon, Yoonsik},
        Title = {Larch/{S}malltalk: A Specification Language for {S}malltalk},
       School = {Iowa State University},
         Year = 1991
)

@InProceedings(	Chetali92,
       Author = {Chetali, Boutheina and Lescanne, Pierre},
        Title = {An Exercise in {LP}: the Proof of a Nonrestoring Division
	         Circuit},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)


@InProceedings(	Choppy92,
       Author = {Choppy, Christine and Bidoit, Michel},
        Title = {Integrating {ASSPEGIQUE} and {LP}},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)


@TechReport(	Detlefs90,
       Author = {Detlefs, David~L.},
        Title = {Concurrent, Atomic Garbage Collection},
  Institution = {Carnegie Mellon University},
         Note = {Ph.~D. Thesis, Department of Computer Science},
         Type = {TR},
       Number = {CS--90--177},
        Month = {October},
         Year = 1990,
)

@InProceedings(	Engberg92,
       Author = {Engberg, Urban and Gr{\o}nning, Peter and Lamport, Leslie},
        Title = {Mechanical Verification of Concurrent Systems with {TLA}},
    BookTitle = {Workshop on Computer Aided Verification}, 
         Year = 1992,
         Note = {Revised version in \cite{Martin92}}
)

  Institution = {Carnegie Mellon University},
         Note = {Ph.~D. Thesis, Department of Computer Science},
         Type = {TR},
       Number = {CS--90--177},
        Month = {October},
         Year = 1990,
)


@TechReport(	Evans94a,
       Author = {Evans, David},
	Title = {Using Specifications to Check Source Code},
         Note = {SM Thesis},
  Institution = {MIT Department of Electrical Engineering and
                 Computer Science},
       Number = {MIT/LCS/TR--628},
	Month = {June},
	 Year = {1994}
)

@InProceedings( Evans94b,
       Author = {Evans, David and Guttag, John~V. and Horning, James~J. and
		 Tan, Yang Meng},
        Title = {{LCLint}: A tool for using specifications to check code},
    BookTitle = {Symposium on the Foundations of Software Engineering},
        Month = {December},
         Year = {1994}
)

@InProceedings( Evans96,
       Author = {Evans, David},
        Title = {Static detection of dynamic memory errors},
    BookTitle = {{SIGPLAN} Conference on Programming Language Design and
		 Implementation, {PLDI'96}},
      Address = {Philadelphia, PA},
        Month = {May},
         Year = {1996}
)

@InProceedings(	Feldman92,
       Author = {Feldman, Gary and Wild, Joseph},
        Title = {The {DEC}spec Project: Tools for {L}arch/{C}},
    BookTitle = {Fifth International Workshop on Computer-Aided Software 
		 Engineering},
      Address = {Montreal},
	Month = {July},
	 Year = 1992,
         Note = {Revised version in \cite{Martin92}}
)

@InProceedings(	Garland88a,
       Author = {Garland, Stephen~J. and Guttag, John~V.},
        Title = {Inductive Methods for Reasoning about Abstract Data Types},
    BookTitle = {15th ACM Symposium on Principles of Programming Languages}, 
      Address = {San Diego},
        Month = {January},
         Year = 1988,
	Pages = {219--228}
)

@InProceedings(	Garland89,
       Author = {Garland, Stephen~J. and Guttag, John~V.},
        Title = {An Overview of {LP}, the {L}arch {P}rover},
    Booktitle = {Third International Conference on Rewriting Techniques and 
		 Applications},
      Address = {Chapel Hill},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~355},
         Year = 1989,
	Pages = {137--151},
)

@InProceedings(	Garland90c,
       Author = {Garland, Stephen~J. and Guttag, John~V.},
        Title = {Using {LP} to Debug Specifications},
 Organization = {IFIP WG2.2/2.3},
    BookTitle = {Programming Concepts and Methods},
      Address = {Sea of Galilee, Israel},
       Editor = {Broy, M. and Jones, C.~B.},
    Publisher = {North-Holland},
        Month = {April 2--5},
         Year = 1990,
        Pages = {369--386},
	 Note = {Superseded by \cite{Garland90b}}
)

@TechReport(	Garland91,
       Author = {Garland, Stephen~J. and Guttag, John~V.},
        Title = {A Guide to {LP}, The {L}arch {P}rover},
  Institution = {DEC Systems Research Center},
      Address = {Palo Alto, CA},
         Type = {Report},
       Number = 82,
        Month = {December},
         Year = 1991,
)

@Article(	Garland90b,
       Author = {Garland, Stephen~J. and Guttag, John~V. and Horning, 
                 James~J.},
        Title = {Debugging {L}arch {S}hared {L}anguage Specifications},
      Journal = {IEEE Transactions on Software Engineering},
       Volume = 16,
       Number = 9,
        Month = {September},
         Year = 1990,
        Pages = {1044--1075},
         Note = {Reprinted as DEC Systems Research Center Report 60.
		 Superseded by Chapter 7 in \cite{Guttag93}}
)

@InProceedings(	Garland93,
       Author = {Garland, Stephen~J. and Guttag, John~V. and 
                 Horning, James~J.},
        Title = {An Overview of {L}arch},
    Booktitle = {Functional Programming, Concurrency, Simulation and Automated 
                 Reasoning},
       Editor = {Lauer, Peter~E.},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~693},
         Year = 1993,
	Pages = {329--348},
)
@InProceedings(	Garland88c,
       Author = {Garland, Stephen~J. and Guttag, John~V. and Staunstrup, 
		 J{\o}rgen~A.},
        Title = {Verification of {VLSI} Circuits using {LP}},
 Organization = {IFIP WG 10.2},
    BookTitle = {The Fusion of Hardware Design and Verification}, 
      Address = {Glasgow},
    Publisher = {North Holland},
	Month = {July 4--6},
         Year = 1988,
	Pages = {329--345}
)

@Manual(	Garland95,
       Author = {Garland, Stephen~J. and Guttag, John~V.},
        Title = {{LP}, the {L}arch {P}rover: Version 3.1},
 Organization = {MIT Laboratory for Computer Science},
        Month = {January},
         Year = 1995,
	 Note = {Available as 
		 http://larch.lcs.mit.edu:8001/larch/LP/overview.html}
)

@Book(		Gehani86,
       Editor = {Gehani, Narain and  McGettrick, Andrew},
        Title = {Software Specification Techniques}, 
    Publisher = {Addison-Wesley}, 
	 Year = 1986
)

@TechReport(	Gong89,
       Author = {Gong, Chun and Wing, Jeannette~M.},
        Title = {Raw Code, Specification, and Proofs of the {A}valon Queue 
                 Example},
  Institution = {Carngie Mellon University},
         Type = {TR},
       Number = {CMU--CS--89-172},
        Month = {August},
         Year = 1989
)

@Article(	Guaspari90,
       Author = {Guaspari, David and Marceau, Carla and Polak, Wolfgang},
        Title = {Formal Verification of {A}da},
      Journal = {IEEE Transactions on Software Engineering},
       Volume = 16,
       Number = 9,
        Month = {September},
         Year = 1990,
	Pages = {1058--1075}
)

@InProceedings(	Guaspari92,
       Author = {Guaspari, David and Marceau, Carla and Polak, Wolfgang},
        Title = {Formal Verification of {A}da Programs},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@InCollection(	Guttag74,
       Author = {Guttag, John~V.},
        Title = {Dyadic specification and its Impact on Reliability},
    Booktitle = {Three Approaches to Reliable Software: Language Design
                 Dyadic Specification, Complementary Semantics}, 
       Editor = {Donahue, J.~E. and Gannon, J.~D. and Guttag J.~V. and
		 Horning, J.~J.},
    Publisher = {University of Toronto},
         Note = {TR~CSRG--45}, 
        Month = {December},
         Year = 1974
)

@PhDThesis(	Guttag75,
       Author = {Guttag, John~V.},
        Title = {The Specification and Application to Programming of Abstract 
		 Data Types},
       School = {University of Toronto, Department of Computer Science},
         Year = 1975
)

@InProceedings(	Guttag79,
       Author = {Guttag, John~V.},
	Title = {Notes on Type Abstraction},
    Booktitle = {Conference on Specifications of Reliable Software}, 
	 Year = 1979,
	 Note = {Reprinted in \cite{Gehani86}}
)
    
@Article(	Guttag78a,
       Author = {Guttag, John~V. and Horning, James~J.},
        Title = {The Algebraic Specification of Abstract Data Types},
      Journal = {Acta Informatica},
       Volume = 10,
       Number = 1, 
         Year = 1978
)

@InProceedings(	Guttag80,
       Author = {Guttag, John~V. and Horning, James~J.},
        Title = {Formal Specification as a Design Tool},
    BookTitle = {7th ACM Symposium on Principles of Programming Languages},
      Address = {Las Vegas},
        Month = {January},
         Year = 1980,
	Pages = {251--261},
         Note = {Reprinted in \cite{Gehani86}}
)

@InProceedings(	Guttag86,
       Author = {Guttag, John~V. and Horning, James~J.},
        Title = {An Introduction to the {L}arch {S}hared {L}anguage},
    BookTitle = {IFIP Ninth World Computer Conference},
      Address = {Paris},
        Month = {September},
         Year = 1986,
	Pages = {809--814},
	 Note = {Superseded by Chapter 3 of \cite{Guttag93}}
)

@Article(	Guttag86a,
       Author = {Guttag, John~V. and Horning, James~J.},
        Title = {Report on the {L}arch {S}hared {L}anguage},
      Journal = {Science of Computer Programming},
       Volume = 6,
       Number = 2,
	Month = {March},
         Year = 1986,
	 Note = {Superseded by \cite{Guttag90} and Chapter 4 of 
                 \cite{Guttag93}}
)

@Article(	Guttag86b,
       Author = {Guttag, John~V. and Horning, James~J.},
        Title = {A {L}arch {S}hared {L}anguage Handbook},
      Journal = {Science of Computer Programming},
       Volume = 6,
       Number = 2,
	Month = {March},
         Year = 1986,
	 Note = {Superseded by Appendix A of \cite{Guttag93}}

)

@TechReport(	Guttag91,
       Author = {Guttag, John~V. and Horning, James~J.},
        Title = {{LCL}: A {L}arch Interface Language for {C}},
  Institution = {DEC Systems Research Center},
      Address = {Palo Alto, CA},
         Type = {Report},
       Number = 74,
        Month = {July},
         Year = 1991,
	 Note = {Superseded by Chapter 5 of \cite{Guttag93}}
)

@InProceedings(	Guttag91a,
       Author = {Guttag, John~V. and Horning, James~J.},
        Title = {A Tutorial on {L}arch and {LCL}, a {Larch/C} Interface 
                 Language},
    BookTitle = {VDM91: Formal Software Development Methods},
      Address = {Delft},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~551},
       Editor = {Prehn, S. and Toetenel, W.~J.},
        Month = {October},
         Year = 1991,
	 Note = {Superseded by Chapter 3 of \cite{Guttag93}}
)

@Book(		Guttag93,
       Editor = {Guttag, John~V. and Horning, James~J.},
         Note = {With Stephen~J. Garland, Kevin~D. Jones, Andr\'es Modet,
		 and Jeannette~M. Wing},
	Title = {Larch: Languages and Tools for Formal Specification},
    Publisher = {Springer-Verlag},
       Series = {Texts and Monographs in Computer Science},
         Year = 1993
)

@InProceedings( Guttag93a,
       Author = {Guttag, John~V.},
        Title = {Goldilocks and the Three Specifications},
    BookTitle = {Proceedings of {TAPSOFT} '93},
    Publisher = {Springer-Verlag},
        Month = {April},
         Year = {1993}
)

@TechReport(	Guttag90,
       Author = {Guttag, John~V. and Horning, James~J. and Modet, Andr\'es},
        Title = {Report on the {L}arch {S}hared {L}anguage: Version 2.3},
         Type = {Report},
       Number = 58,
  Institution = {DEC Systems Research Center},
      Address = {Palo Alto, CA},
        Month = {April 14},
         Year = 1990,
	 Note = {Superseded by Chapter 4 of \cite{Guttag93}}
)

@Article(	Guttag85,
       Author = {Guttag, John~V. and Horning, James~J. and Wing, 
                 Jeannette~M.},
        Title = {The {L}arch Family of Specification Languages},
      Journal = {IEEE Software},
       Volume = 2,
       Number = 5,
         Year = 1985,
        Pages = {24--36},
	 Note = {Superseded by Chapter 3 of \cite{Guttag93}}
)

@TechReport(	Guttag85a,
       Author = {Guttag, John~V. and Horning, James~J. and Wing, 
                 Jeannette~M.},
        Title = {Larch in Five Easy Pieces},
  Institution = {DEC Systems Research Center},
      Address = {Palo Alto, CA},
         Type = {Report},
       Number = 5,
        Month = {July},
         Year = 1985,
	 Note = {Superseded by \cite{Guttag93}}
)

@MastersThesis(	Hinman87,
       Author = {Hinman, David},
        Title = {On the Design of {L}arch Interface Languages},
       School = {Department of Electrical Engineering and Computer Science, 
	         MIT},
        Month = {January},
         Year = 1987
)

@InProceedings(	Horning85,
       Author = {Horning, James~J.},
        Title = {Combining Algebraic and Predicative Specifications in 
                 {L}arch},
    BookTitle = {International Joint Conference on Theory and Practice of
		 Software Development, TAPSOFT},
      Address = {Berlin},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~186},
        Month = {March},
         Year = 1985,
	Pages = {12--26},
	 Note = {Superseded by \cite{Guttag93}}
)

@InProceedings( Horning95,
       Author = {Horning, James~J.},
        Title = {The {L}arch {S}hared {L}anguage: Some Open Problems},
    BookTitle = {Recent Trends in Data Type Specification},
       Editor = {Haveraaen, Magne and Owe, Olaf and Dahl, Ole-Johan},
      Address = {Berlin},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~1130},
         Year = 1996,
         Note = {11th Workshop on Specification of Abstract Data Types,
		 Joint with the 8th COMPASS Workshop, Oslo, Norway,
		 September 1995, Selected Papers, ISSN 0302-9743,
		 ISBN 3-540-61629-2}
)


@TechReport(	Jones91,
       Author = {Jones, Kevin~D.},
        Title = {{LM3}: A {L}arch Interface Language for {M}odula-3: Version 
		 1.0},
  Institution = {DEC Systems Research Center},
      Address = {Palo Alto, CA},
         Type = {Report},
       Number = 72,
        Month = {June},
         Year = 1991
)

@InProceedings(	Jones92a,
       Author = {Jones, Kevin~D.},
	Title = {A Semantics for a {L}arch/{M}odula-3 Interface Language},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@Unpublished(	Jones92,
       Author = {Jones, Kevin~D.},
	Title = {{LM3} Reference Manual},
	 Note = {In preparation}
)

@TechReport(	Laux92,
       Author = {Laux, Michael~R. and Bourdeau, Robert~H. and Cheng, 
		 Betty~H.~C.},
	Title = {An Integrated Environment Supporting the Reuse of Formal
      		 Specifications},
  Institution = {Michigan State University, Deptartment of Computer Science}, 
	 Type = {TR},
       Number = {MSU--CPS--ACS--70},
        Month = {September},
         Year = 1992
)

@InProceedings(	Leavens92,
       Author = {Leavens, Gary~T. and Cheon, Yoonsik},
	Title = {Preliminary Design of {L}arch/{C}++},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@PhDThesis(	Lerner91,
       Author = {Lerner, Richard Allen},
        Title = {Specifying Objects of Concurrent Systems},
       School = {School of Computer Science, Carnegie Mellon University},
         Year = 1991,
        Month = {May},
         Note = {TR CMU--CS--91--131}
)

@InProceedings(	Lescanne83,
       Author = {Lescanne, Pierre},
	Title = {Computer Experiments with the {REVE} Term-Rewriting System 
		 Generator},
    BookTitle = {Tenth ACM Symposium on Principles of Programming Languages}, 
	 Year = 1983
)

@Book(		Liskov86,
       Author = {Liskov, Barbara and Guttag, John~V.},
        Title = {Abstraction and Specification in Program Development},
    Publisher = {MIT Press},
      Address = {Cambridge, MA},
       Series = {The MIT Electrical Engineering and Computer Science Series},
         Year = 1986
)

@InProceedings( Luchangco94,
       Author = {Luchangco, Victor and S\"oylemez, Ekrem  and Garland,
                 Stephen~J. and Lynch, Nancy~A.},
        Title = {Verifying Timing Properties of Concurrent Algorithms},
    BookTitle = {{FORTE'94}: Seventh International Conference on Formal 
                 Description Techniques for Distributed Systems and 
		 Communication Protocols},
      Address = {Berne, Switzerland},
    Publisher = {Chapman and Hall},
        Month = {October 4--7},
	 Year = {1994},
	Pages = {259--273}
)

@InProceedings(	Martin90,
       Author = {Martin, Ursula and Nipkow, Tobias},
        Title = {Automating {S}quiggol},
 Organization = {IFIP WG2.2/2.3},
    BookTitle = {Programming Concepts and Methods},
      Address = {Sea of Galilee, Israel},
       Editor = {Broy, M. and Jones, C.~B.},
    Publisher = {North-Holland},
        Month = {April 2--5},
         Year = 1990,
	Pages = {223--236}
)

@Proceedings(	Martin92,
        Title = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
      Address = {Dedham, MA},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@InProceedings(	Mellergaard92,
       Author = {Mellergaard, Niels and Staunstrup, J{\o}rgen~A.},
	Title = {Generating  Proof Obligations for Circuits},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@Book(		Nelson91,
       Editor = {Nelson, Greg},
	Title = {Systems Programming with Modula-3},
    Publisher = {Prentice Hall}, 
	 Year = 1991
)

@InProceedings( Petrov96,
       Author = {Petrov, Tsvetomir~P. and Pogosyants, A. and and Garland,
                 Stephen~J. and Luchangco, Victor and Lynch, Nancy~A.},
        Title = {Computer-assisted verification of an algorithm for concurrent
		 timestamps},
    Booktitle = {Formal Description Techniques XI: Theory, Application, and
		 Tools},
       Editor = {Gotzhein, Reinhard and Bredereke, Jan},
      Address = {Kaiserslautern, Germany},
    Publisher = {Chapman and Hall},
        Month = {October 8--11},
	 Year = {1996},
	Pages = {29--44},
         Note = {{FORTE/PSTV'96}: Joint International Conference on Formal 
                 Description Techniques for Distributed Systems and 
		 Communication Protocols, and Protocol Specification, Testing,
		 and Verification},
)

@InProceedings(	Rollins91,
       Author = {Rollins, Eugene~J. and Wing, Jeannette~M.},
	Title = {Specifications as Search Keys for Software Libraries},
    Booktitle = {International Conference on Logic Programming}, 
      Address = {Paris}, 
	Month = {June},
	 Year = 1991
)

@InProceedings(	Saxe92,
       Author = {Saxe, James~B. and Garland, Stephen~J. and Guttag, John~V. and
		 Horning, James~J.},
        Title = {Using Transformations and Verification in Circuit Design},
    Booktitle = {International Workshop on Designing Correct Circuits},
    Publisher = {North-Holland, IFIP Transactions A-5},
       Editor = {Staunstrup, J. and Sharp, R.},
         Year = 1992,
         Note = {Also published as DEC Systems Research Center Report 78, 
		 September 1991.  Reprinted in \cite{Martin92}.  
		 Superseded by \cite{Saxe93}.}
)

@Article(	Saxe93,
       Author = {Saxe, James~B. and Garland, Stephen~J. and Guttag, John~V. and
		 Horning, James~J.},
        Title = {Using Transformations and Verification in Circuit Design},
      Journal = {Formal Methods in System Design},
       Volume = {3},
       Number = {3},
	Month = {December},
         Year = 1993,
	Pages = {181--209}
)

@InProceedings(	Scott92,
       Author = {Scott, Elizabeth~A. and Norrie, K.~J.},
	Title = {Using {LP} to Study the Language {PL}},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992,
)

@InProceedings(	Sogaard93,
       Author = {S{\o}gaard-Anderson, J{\o}rgen~F. and Garland, Stephen~J. and 
		 Guttag, John~V. and Lynch, Nancy~A. and Pogosyants, Anna},
	Title = {Computed-Assisted Simulation Proofs},
    Booktitle = {Fifth Conference on Computer-Aided Verification},
      Address = {Heraklion, Crete},
	Month = {June},
 	 Year = 1993,
       Editor = {Costas Courcoubetis},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~697},
	Pages = {305--319}
)

@MastersThesis(	Soylemez94,
       Author = {S\"oylemez, Ekrem},
	Title = {Automatic Verification of the Timing Properties of {MMT }
		 Automata},
       School = {Department of Electrical Engineering and Computer Science, 
	         MIT},
	Month = {February},
	 Year = {1994}
)

@InProceedings(	Stata95,
       Author = {Stata, Raymie and Guttag, John~V.},
	Title = {Modular reasoning in the presence of subclassing},
    BookTitle = {Object-Oriented Programming Systems, Languages, and
		 Applications},
	Month = {October},
	 Year = 1995
)

@PhDThesis(	Stata96,
       Author = {Stata, Raymond Paul},
        Title = {Modularity in the Presence of Subclassing},
       School = {Department of Electrical Engineering and Computer Science, 
	         MIT},
	Month = {June},
	 Year = {1996}
)

@InProceedings(	Staunstrup89,
       Author = {Staunstrup, J{\o}rgen~A. and Garland, Stephen~J. and Guttag,
		 John~V.},
        Title = {Localized Verification of Circuit Descriptions},
    BookTitle = {International Workshop on Automatic Verification Methods for 
		 Finite State Systems},
      Address = {Grenoble},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~407},
	Month = {June},
         Year = 1989,
        Pages = {349--364}
)

@InProceedings(	Staunstrup92,
       Author = {Staunstrup, J{\o}rgen~A. and Garland, Stephen~J. and Guttag,
		 John~V.},
        Title = {Mechanized Verification of Circuit Descriptions using the 
		 {L}arch {P}rover},
 Organization = {IFIP TC10/WG10.2},
    BookTitle = {Theorem Provers in Circuit Design},
      Address = {Nijmegen, The Netherlands},
       Editor = {Stavridou, V. and Melham, T.~F. and Boute, R.~T.},
    Publisher = {North-Holland, IFIP Transactions A-10},
        Month = {June},
         Year = 1992,
	Pages = {277--299}
)

@InProceedings(	Tan92,
       Author = {Tan, Yang Meng},
	Title = {Semantic Analysis of {L}arch Interface Specifications},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@InProceedings(	Tan94a,
       Author = {Tan, Yang Meng},
	Title = {Interface Language for Supporting Programming Styles},
    BookTitle = {{POPL} Workshop on Interface Definition Languages},
      Address = {Portland, Oregon},
        Month = {January},
         Year = 1994
)

@PhDThesis(	Tan94b,
       Author = {Tan, Yang Meng},
	Title = {Formal Specification Techniques for Promoting Software
		Modularity, Enhancing Documentation, and Testing 
		Specifications},
       School = {Department of Electrical Engineering and Computer Science, 
	         MIT},
	Month = {May},
	 Year = {1994},
	 Note = {MIT/LCS/TR--619}
)

@Book(		Tan95,
       Author = {Tan, Yang Meng},
	Title = {Formal Specification Techniques for Engineering Modular {C}},
    Publisher = {Kluwer International Series in Software Engineering},
       Volume = 1,
      Address = {Boston},
	 Year = {1995}
)


@Unpublished(	Taylor90,
       Author = {Taylor, David~S.},
        Title = {A Beginner's Strategy Guide to the {L}arch {P}rover},
         Note = {S.~B. Thesis, Department of Electrical Engineering and 
		 Computer Science, MIT},
        Month = {May},
         Year = 1990
)

@InProceedings(	Vandevoorde92,
       Author = {Vandevoorde, Mark~T.},
	Title = {Optimizing Programs with Partial Specifications},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@InProceedings( Vandevoorde93,
       Author = {Vandevoorde, Mark~T.},
        Title = {Specifications Can Make Programs Run Faster},
    BookTitle = {Proceedings of {TAPSOFT} '93},
    Publisher = {Springer-Verlag},
        Month = {April},
         Year = {1993}
)

@TechReport(	Vandevoorde94a,
       Author = {Vandevoorde, Mark~T.},
        Title = {Exploiting Specifications to Improve Program Performance},
  Institution =	{MIT},
       Number = {LCS/TR--598},
         Year = 1994,
	Month = {February},
         Note = {Ph.~D. Thesis, Department of Electrical Engineering and
		 Computer Science}
)

@InProceedings( Vandevoorde94b,
       Author = {Vandevoorde, Mark~T. and Guttag, John~V.},
        Title = {Using specialized procedures and specification-based analysis 
		 to reduce the runtime costs of modularity},
    BookTitle = {Symposium on the Foundations of Software Engineering},
        Month = {December},
         Year = {1994}
)

@InProceedings( Vandevoorde96,
       Author = {Vandevoorde, Mark~T. and Kapur, Deepak},
        Title = {Distributed {L}arch {P}rover ({DLP}): an experiment in
		 parallelizing a rewrite-rule based prover},
    BookTitle = {Rewriting Techniques and Applications},
        Month = {July},
         Year = {1996}
)

@Unpublished(	Vogt90,
       Author = {Vogt, Mary~A.},
        Title = {Extension of the {L}arch {P}rover by a Method of Inference 
		 Using Linear Arithmetic},
         Note = {S.~B. Thesis, Department of Electrical Engineering and 
		 Computer Science, MIT},
        Month = {September},
         Year = 1990
)

@InProceedings(	Voisin92,
       Author = {Voisin, Frederic},
	Title = {A New Front-end for the {L}arch {P}rover},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@TechReport(	Wing83,
       Author = {Wing, Jeannette~M.},
        Title = {A Two-Tiered Approach to Specifying Programs},
  Institution =	{MIT},
       Number = {LCS/TR--299},
         Year = 1983,
	Month = {May},
         Note = {Ph.~D. Thesis, Department of Electrical Engineering and
		 Computer Science}
)

@InProceedings(	Wing87,
       Author = {Wing, Jeannette~M.},
        Title = {A {L}arch Specification of the Library Problem},
    BookTitle = {Fourth International Workshop on Software Specifications and 
		 Design},
      Address = {Monterey},
        Month = {April},
         Year = 1987,
	Pages = {34--41},
         Note = {Also available as CMU--CS--86--168, December 1986}
)

@Article(	Wing87a,
       Author = {Wing, Jeannette~M.},
        Title = {Writing {L}arch Interface Language Specifications},
      Journal = {ACM Transactions on Programming Languages and Systems},
       Volume = 9,
       Number = 1,
        Month = {January},
         Year = 1987,
	Pages = {1--24}
)

@InProceedings(	Wing88,
       Author = {Wing, Jeannette~M.},
        Title = {Specifying Recoverable Objects},
	Pages = {317--331},
    BookTitle = {Sixth Annual Northwest Software Quality Conference},
      Address = {Portland, OR},
        Month = {September},
         Year = 1990,
         Note = {Also available as CMU--CS--88--170, August 1988}
)

@InProceedings(	Wing89a,
       Author = {Wing, Jeannette~M.},
        Title = {Specifying {A}valon Objects in {L}arch},
    Booktitle = {International Joint Conference on Theory and Practice of
		 Software Development, TAPSOFT},
      Address = {Barcelona},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~352},
        Month = {March 13--17},
         Year = 1989,
	Pages = {61--80},
	 Note = {Also available as CMU--CS--88--208, December 1988}
)

@Article(	Wing90,
       Author = {Wing, Jeannette~M.},
        Title = {Using {L}arch to Specify {A}valon/{C}++ Objects},
      Journal = {IEEE Transactions on Software Engineering},
       Volume = 16,
       Number = 9,
        Month = {September},
         Year = 1990,
	Pages = {1076--1088},
         Note = {Revised version in \cite{Wing89a}}
)

@TechReport(	Wing89,
       Author = {Wing, Jeannette~M. and Gong, Chun},
        Title = {Machine-Assisted Proofs of Properties of {A}valon Programs},
  Institution = {Carnegie Mellon University},
         Type = {TR},
       Number = {CMU--CS--89--171},
        Month = {August},
         Year = 1989
)

@InProceedings(	Wing90a,
       Author = {Wing, Jeannette~M. and Gong, Chun},
        Title = {Experience with the {L}arch {P}rover},
  Institution = {ACM},
    BookTitle = {Workshop on Formal Methods in Software Development},
        Month = {May},
         Year = 1990,
	Pages = {140--143}
)

@InProceedings(	Wing92,
       Author = {Wing, Jeannette~M. and Rollins, Eugene and Zaremski, Amy 
		 Moormann},
	Title = {Thoughts on a {L}arch/{ML} and a New Application for {LP}},
    BookTitle = {First International Workshop on Larch},
       Editor = {Martin, Ursula and Wing, Jeannette~M.},
    Publisher = {Springer-Verlag},
        Month = {July},
         Year = 1992
)

@InProceedings(	Wing91,
       Author = {Wing, Jeannette~M. and Zaremski, Amy Moormann},
        Title = {A Formal Specification of a Visual Language Editor},
    BookTitle = {Sixth International Workshop on Software Specification and 
		 Design},
      Address = {Como, Italy},
        Month = {October},
         Year = 1991,
         Note = {Also available as CMU--CS--91--112, February 1991}
)

@InProceedings(	Wing91a,
       Author = {Wing, Jeannette~M. and Zaremski, Amy Moormann},
	Title = {Unintrusive Ways to Integrate Formal Specifications in 
		 Practice},
    Booktitle = {VDM91: Formal Software Development Methods},
      Address = {Delft},
       Editor = {Prehn, S. and Toetenel, W.~J.},
    Publisher = {Springer-Verlag Lecture Notes in Computer Science~551},
	Month = {October},
	 Year = 1991
)

@TechReport(	Zaremski91,
       Author = {Zaremski, Amy Moormann},
        Title = {A {L}arch Specification of the {M}iro Editor},
  Institution = {Carnegie Mellon University},
       Number = {CMU--CS--91--112},
        Month = {February},
         Year = 1991
)