Part 1 Modelling and specification: some mathematical thoughts on languages for data directed design, E. Wagner; algebraic alternative for compiler construction, T. Rus; algebraic semantics and monad theory, E. Badouel; an illustrated mathematical foundation for ERA, C.N.G. Dampney et al; on the expressiveness of equational type logic, V. Manca et al; linear term rewriting systems are higher dimensional string rewriting systems, M. Johnson; inductive reasoning for completing equational software specifications, K.P. Jantke; term induction proofs by a generalization of narrowing, U. Fraus and H. Hussmann. Part 2 Formal methods in software development: prototyping and formal specifications, C. Choppy; development of modular specifications by stepwise refinements using the PLUSS specification language, M. Bidoit; software complexity measures, programming methodologies, and the size of machines, J.C. Cherniavsky and C.H. Smith; the implementation of Z specifications using program transformation systems - the SuZan Project, R. Knott and P. Krause; the systematic reduction of VDM specifications, A.P. French et al; experiences with using formal specification techniques for operations research problems, A.P. French et al; a survey of temporal logic methods in system development, N.J. Wilson. Part 3 Specification for communication and concurrency: integrating automata and temporal logic - a framework for specification of real-time systems and software, A. Gabrielian and R. Iyer; specification and derivation of process networks, F. Carrez and D. Mery; algebraic term nets - a formalism for specifying communications software in the OSI framework, M. Bettaz and A. Choutri; using LOTOS in the object-based development of embedded systems, R.G. Clark; a data type specification for the process part of basic LOTOS - an axiomatic semantics, G.H.B. Rafsanjani; modelling of LOTOS specifications by Petri Nets, G.H.B. Rafsanjani. Part 4 Program verification and development: modules and verification, G. Antoniou; program analysis by symbolic execution and generalization, G. Colman et al; proving and developing concurrent programs - a small system, D. Mery; automated proof and program development, D. Galmiche and O. Hermann; interactive automated verification of functional programming languages, R.B. Hughes and R.M. Zimmer; theorem proving and program synthesis with Oyster, C. Horn and A. Smaill; the PICT system, A.G. Hamilton; an interactive tool for deriving correct programs, L. Groves and R. Nickson.
