Selected publications of Stephen J. Garland

Joshua A. Tauber and Stephen J. Garland. "Definition and expansion of composite automata in IOA," in progress.

Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun K. Kaynar, and Nancy Lynch. "Using simulated execution in verifying distributed algorithms," Software Tools for Technology Transfer (2003) 4, pages 1-10. Extended abstract appeared in Proceedings of Fourth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2003), New York, January 2003.

Andrej Bogdanov, Stephen J. Garland, and Nancy A. Lynch. "Mechanical translation of I/O automata specifications into first-order logic," Formal Techniques for Networked and Distribued Systems, FORTE 2002, Houston, Texas, November 11-14, 2002, Lecture Notes in Computer Science 2529, Doron A. Peled and Moshe Y. Vardi (editors), Springer-Verlag, pages 364-368.

Dilsun Kirli Kaynar, Anna Chefter, Laura Dean, Stephen J. Garland, Nancy A. Lynch, Toh Ne Win, and Antonio Ramirez-Robredo. "Simulating nondeterministic systems at multiple levels of abstraction," Proceedings of Tools Day, held in conjunction with CONCUR 2002, Brno, Czech Republic, August 4, 2002.

Dilsun Kirli Kaynar, Anna Chefter, Laura Dean, Stephen J. Garland, Nancy A. Lynch, Toh Ne Win, and Antonio Ramirez-Robredo. "The IOA simulator," Technical Report MIT-LCS-TR-843, MIT Laboratory for Computer Science, Cambridge, MA, July 2002.

Stephen J. Garland and Nancy A. Lynch. "Using I/O automata for developing distributed systems," Foundations of Component-Based Systems, Gary T. Leavens and Murali Sitaraman, editors, Cambridge University Press, 2000, pages 285-312.
Abstract, Paper (pdf, compressed PostScript)

Li-wei H. Lehman, Stephen J. Garland, and David L. Tennenhouse. "Active reliable multicast," Infocom '98, San Francisco, April 1998, IEEE Communications Society.
Abstract

Stephen J. Garland, Nancy A. Lynch, and Mandana Vaziri. "IOA: a language for specifying, programming, and validating distributed systems," MIT Laboratory for Computer Science, 1997.
Paper

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 (pdf, compressed PostScript)

Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy 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, Paper (pdf, compressed PostScript)

Jørgen F. Søgaard-Andersen, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anya Pogosyants, "Computed-assisted simulation proofs," Computer-Aided Verification, Fifth International Conference, CAV '93, Elounda, Greece, June/July 1993, Lecture Notes in Computer Science 697, Costas Courcoubetis (editor), Springer-Verlag, pages 305-319.
Abstract Paper (pdf, compressed PostScript)

Stephen J. Garland, John V. Guttag, and James J. Horning, "An overview of Larch," Functional Programming, Concurrency, Simulation, and Automated Reasoning, Lecture Notes in Computer Science 693, Peter E. Lauer (editor), Springer-Verlag, 1993, pages 329-348.
Abstract, Paper

John V. Guttag and James J. Horning (editors), with Stephen J. Garland, Kevin D. Jones, Andres Modet, and Jeannette M. Wing, Larch: Languages and Tools for Formal Specification, Springer-Verlag Texts and Monographs in Computer Science, 1993.

Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag, "Mechanized verification of circuit descriptions using the Larch Prover," Theorem Provers in Circuit Design, Nijmegen, The Netherlands, June 22-24, 1992, North-Holland IFIP Transactions A-10, V. Stavridou, T. F. Melham, and R. T. Boute (editors), pages 277-299.
Abstract

Katherine A. Yelick and Stephen J. Garland, "A parallel completion procedure for term rewriting systems," Automated Deduction--CADE-11, Sarasota Springs, NY, June 1992, Lecture Notes in Computer Science 607, D. Kapur (editor), Springer-Verlag, pages 109-123.
Abstract

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.

James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning, "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.

Stephen J. Garland, Introduction to Computer Science with Applications in Pascal, Addison-Wesley Publishing Co., Reading, MA, 1985.