Abstract is missing.
- Diagrams and Programming Languages for Programmable ControllersStuart Anderson, Konstantinos Tourlas. 1-19
- Graphical Specification and Reasoning: Case Study Generalised Railroad CrossingHenning Dierks, Cheryl Dietz. 20-39
- A Graphic Notation for Formal Specifications of Dynamic SystemsGianna Reggio, Mauro Larosa. 40-61
- A Semantic Integration of Object-Z and CSP for the Specification of Concurrent SystemsGraeme Smith. 62-81
- Class Refinement and Interface Refinement in Object-Oriented ProgramsAnna Mikhajlova, Emil Sekerinski. 82-101
- Formalizing Requirements for Distributed Systems with Trace DiagramsStephan Kleuker. 102-121
- Consistent Graphical Specification of Distributed SystemsFranz Huber, Bernhard Schätz, Geralf Einert. 122-141
- Design of Reactive Control Systems for Event-Drivem OperationsKevin Lano, Ana Sánchez. 142-161
- An M-Net Semantics for a Real-Time Extension of µSDLHans Fleischhack, Josef Tapken. 162-181
- Reconciling Real-Time with Asynchronous Message PassingManfred Broy, Radu Grosu, Cornel Klein. 182-200
- Specifying the Remote Control of Valves in an Explosion Test EnvironmentMartin Schönhoff, Mojgan Kowsari. 201-220
- PICGAL: Practical Use of Formal Specification to Develop a Complex Critical SystemLionel Devauchelle, Peter Gorm Larsen, Henrik Voss. 221-236
- Mathematical Modeling and Analysis of an External Memory ManagerWilliam D. Young, William R. Bevier. 237-257
- Automatic Translation of VDM-SL Specifications into GoferPaul Mukherjee. 258-277
- Towards an Integrated CASE and Theorem Proving Tool for VDM-SLSten Agerholm, Jacob Frost. 278-297
- Specification of Required Non-determinismKevin Lano, Juan Bicarregui, José Luiz Fiadeiro, Antónia Lopes. 298-317
- A Corrected Failure Divergence Model for CSP in Isabelle/HOLHaykal Tej, Burkhart Wolff. 318-337
- A Proof Obligation Generator for VDM-SLBernhard K. Aichernig, Peter Gorm Larsen. 338-357
- Verification of Cryptographic Protocols: An ExperimentMarc Mehdi Ayadi, Dominique Bolignano. 358-377
- TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal NotationsJean-Charles Grégoire. 378-397
- A TLA Solution to the Specification and Verification of the RLP1 Retransmission ProtocolAbdelillah Mokkedem, Michael J. Ferguson, Robert de B. Johnston. 398-417
- An Efficient Technique for Deadlock Analysis of Large Scale Process NetworksJ. M. R. Martin, S. A. Jassim. 418-441
- Implementing a Model Checker for LEGOShenwei Yu, Zhaohui Luo. 442-458
- Formal Verification of Transformations for Peephole OptimizationAxel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rueß. 459-472
- A Meta-Method for Formal Method IntegrationRichard F. Paige. 473-494
- Reuse of Verified Design Templates Through Extended Pattern MatchingDavid Hemer, Peter A. Lindsay. 495-514
- A Compositional Proof System for Shared Variable ConcurrencyFrank S. de Boer, Ulrich Hannemann, Willem P. de Roever. 515-532
- A Framework for Modular Formal Specification and VerificationPierre Michel, Virginie Wiels. 533-552
- A Timed Semantics for the STATEMATE Implementation of StatechartsCarsta Petersohn, Luis Urbina. 553-572
- Using PVS to Prove a Z Refinement: A Case StudyDavid W. J. Stringer-Calvert, Susan Stepney, Ian Wand. 573-588
- Verification of Reactive Systems Using DisCo and PVSPertti Kellomäki. 589-604
- Term Rewrite Systems to Derive Set Boolean Operations on 2D ObjectsDavid Cazier, Jean-François Dufourd. 605-623
- A Normal Form Reduction Strategy for Hardware/Software PartitioningLeila Silva, Augusto Sampaio, Edna Barros. 624-643
- Viewpoint Consistency in Z and LOTOS: A Case StudyEerke Boiten, Howard Bowman, John Derrick, Maarten Steen. 644-664
- A UNITY Mapping Operator for Distributed ProgramsMichel Charpentier. 665-684