Abstract is missing.
- Is Engineering Software Amenable to Formal Specification?John W. Baugh Jr.. 1-17
- How to Prove Observational Theorems with LPMichel Bidoit, Rolf Hennicker. 18-35
- Using SOS Definitions in Term Rewriting ProofsKarl-Heinz Buth. 36-54
- An Exercise in LP: The Proof of a Non Restoring Division CircuitBoutheina Chetali, Pierre Lescanne. 55-68
- Integrating ASSPEGIQUE and LPChristine Choppy, Michel Bidoit. 69-85
- Mechanical Verification of Concurrent Systems with TLAUrban Engberg, Peter Grønning, Leslie Lamport. 86-97
- The DECspec Project: Tools for Larch/CGary Feldman, Joseph Wild. 98-103
- Formal Verification of Ada ProgramsDavid Guaspari, Carla Marceau, Wolfgang Polak. 104-141
- A Semantics for a Larch/Modula-3 Interface LanguageKevin D. Jones. 142-158
- Preliminary Design of Larch/C++Gary T. Leavens, Yoonsik Cheon. 159-184
- Generating Proof Obligations for CircuitsNiels Mellergaard, Jørgen Staunstrup. 185-200
- Using Transformations and Verification in Circuit DesignJames B. Saxe, John V. Guttag, James J. Horning, Stephen J. Garland. 201-226
- Using LP to Study the Language PL:::+:::::0::E. A. Scott, K. J. Norrie. 227-245
- Semantic analysis of Larch Interface SpecificationsYang Meng Tan. 246-261
- Optimizing Programs with Partial SpecificationsMark T. Vandevoorde. 262-281
- A New Front-End for the Larch ProverFrédéric Voisin. 282-296
- Thoughts on a Larch/ML and a New Application for LPJeannette M. Wing, Eugene J. Rollins, Amy Moormann Zaremski. 297-312