author : Jim Woodcock

Contents

• C. A. R. Hoare.

Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle

• Cliff B. Jones.

Scientific Decisions which Characterize VDM

• John M. Rushby.

Mechanized Formal Methods: Where Next?

• Joseph Sifakis.

Integration, the Price of Success (extended abstract)

• Michael Jackson.

The Role of Formalism in Method (abstract)

• Eric Conquet, Jean-Luc Marty.

Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project.

• Henk Eertink, Wil Janssen, Paul Oude Luttighuis, Wouter B. Teeuw, Chris A. Vissers.

A Business Process Design Language

• Jan Philipps, Bernhard Rumpe.

Refinement of Pipe-and-Filter Architectures

• John Herbert, Bruno Dutertre, Robert Riemenschneider, Victoria Stavridou.

A Formalization of Software Architecture

• Reino Kurki-Suonio.

Component and Interface Refinement in Closed-System Specifications

• Dusko Pavlovic.

Semantics of First Order Parametric Specifications

• Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan.

A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software

• Frank Reffel, Stefan Edelkamp.

Error Detection with Directed Symbolic Model Checking

• Rajeev Alur, Joel M. Esposito, M. Kim, Vijay Kumar, Insup Lee.

Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination

• Stavros Tripakis, Karine Altisen.

On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems

• Jean-Michel Couvreur.

On-the-Fly Verification of Linear Temporal Logic

• David Deharbe, Anamaria Martins Moreira.

Symbolic Model Checking with Fewer Fixpoint Computations

• Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, Gigliola Vaglini.

Formula Based Abstractions of Transition Systems for Real-Time Model Checking

• Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier.

IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems

• Farn Wang.

Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes

• Denis Sabatier, Pierre Lartigue.

The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications

• Patrick Behm, Paul Benoit, Alain Faivre, Jean-Marc Meynadier.

Meteor: A Successful Application of B in a Large Project

• Brian Matthews, Elvira Locuratolo.

Formal Development of Databases in ASSO and B

• Yann Rouzaud.

Interpreting the B-Method in the Refinement Calculus

• Martin Buchi, Ralph-Johan Back.

Compositional Symmetric Sharing in B

• Cesar Munoz, John M. Rushby.

Structural Embeddings: Mechanization with Method

• Steve Dunne.

The Safe Machine: A New Specification Construct for B

• Michael J. Butler.

csp2B: A Practical Approach to Combining CSP and B

• Salimeh Behnia, Helene Waeselynck.

Test Criteria Definition for B Models

• Richard F. Paige, Eric C. R. Hehner.

Bunches for Object-Oriented, Concurrent, and Real-Time Specification

• Enn Tyugu, Mihhail Matskin, Jaan Penjam.

Applications of Structural Synthesis of Programs

• Michel Charpentier, K. Mani Chandy.

Towards a Compositional Approach to the Design and Verification of Distributed Systems

• Andre Wong, Marsha Chechik.

Formal Modeling in a Commercial Setting: A Case Study

• Igor Burdonov, Alexander Kossatchev, Alexandre Petrenko, Dmitri Galter.

KVEST: Automated Generation of Test Suites from Formal Specifications

• Lydie du Bousquet.

Feature Interaction Detection Using Testing and Model-Checking Experience Report

• Nisse Husberg, Tapio Manner.

Emma: Developing an Industrial Reachability Analyser for SDL

• Jean-Francois Monin, Francis Klay.

Correctness Proof of the Standardized Algorithm for ABR Conformance

• Thomas Arts, Mads Dam.

Verifying a Distributed Database Lookup Manager Written in Erlang

• Fred Gilham, R. A. Riemenschneider, Victoria Stavridou.

Secure Interoperation of Secure Distributed Databases

• Volkmar Lotz, Volker Kessler, Georg Walter.

A Formal Security Model for Microprocessor Hardware

• Steve Schneider.

Abstraction and Testing

• Dan Zhou, Shiu-Kai Chin.

Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol

• Patrick Lincoln, John C. Mitchell, Mark Mitchell, Andre Scedrov.

Probabilistic Polynomial-Time Equivalence and Security Analysis

• Riccardo Focardi, Fabio Martinelli.

A Uniform Approach for the Definition of Security Properties

• Paul F. Syverson, Stuart G. Stubblebine.

Group Principals and the Formalization of Anonymity

• Richard F. Paige, Jonathan S. Ostroff.

Developing BON as an Industrial-Strength Formal Method

• Luis Mandel, Maria Victoria Cengarle.

On the Expressive Power of OCL

• Eric Meyer, Jeanine Souquieres.

A Systematic Approach to Transform OMT Diagrams to a B Specification

• Shaoying Liu.

Verifying Consistency and Validity of Formal Specifications by Testing

• Marine Tabourier, Ana R. Cavalli, Melania Ionescu.

A GSM-MAP Protocol Experiment Using Passive Testing

Contents

• Pascal Poizat, Christine Choppy, Jean-Claude Royer.

From Informal Requirements to COOP: A Concurrent Automata Approach

• Frederic Lang, Pierre Lescanne, Luigi Liquori.

A Framework for Defining Object-Calculi

• Sanjit A. Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, S. D. Dhodapkar.

A Translation of Statecharts to Esterel

• Xia Yong, Chris George.

An Operational Semantics for Timed RAISE

• Heike Wehrheim.

Data Abstraction for CSP-OZ

• Fiona Polack, Susan Stepney.

Systems Development Using Z Generics

full paper

• Perry Alexander, Murali Rangarajan, Phillip Baraona.

A Brief Summary of VSPEC

• Gary T. Leavens, Albert L. Baker.

Enhancing the Pre- and Postcondition Technique for More Expressive Specifications

• Markus Muller-Olm, Andreas Wolf.

On Excusable and Inexcusable Failures

• Richard Verhoeven, Roland Carl Backhouse.

Interfacing Program Construction and Verification

• S. Dellacherie, Samuel Devulder, Jean-Luc Lambert.

Software Verification Based on Linear Programming

• Brendan P. Mahony, Jin Song Dong.

Sensors and Actuators in TCOZ

• Bernd Krieg-Bruckner, Jan Peleska, Ernst-Rudiger Olderog, Alexander Baer.

The UniForM Workbench, a Universal Development Environment for Formal Methods

• Bernhard Schatz, Franz Huber.

Integrating Formal Description Techniques

• Stephan Merz.

A More Complete TLA

• Frank S. de Boer, Ulrich Hannemann, Willem-Paul de Roever.

Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach

• Andrew Martin.

Relating Z and First-Order Logic

• Joao Pedro Sousa, David Garlan.

Formal Modeling of the Enterprise JavaBeansTM Component Integration Framework

• Leonid Mikhajlov, Emil Sekerinski, Linas Laibinis.

Developing Components in the Presence of Re-entrance

• H. B. M. Jonkers.

Communication and Synchronisation Using Interaction Objects

• Loe M. G. Feijs.

Modelling Microsoft COM Using pi-Calculus

• Irina M. Smarandache, Thierry Gautier, Paul Le Guernic.

Validation of Mixed SIGNAL-ALPHA Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints

• Simin Nadjm-Tehrani, Ove Akerlund.

Combining Theorem Proving and Continuous Models in Synchronous Design

• Juliano Iyoda, Augusto Sampaio, Leila Silva.

ParTS: A Partitioning Transformation System

• He Jifeng.

A Behavioral Model for Co-design

• Ana L. C. Cavalcanti, David A. Naumann.

A Weakest Precondition Semantics for an Object-Oriented Language of Refinement

• Ralph-Johan Back, Anna Mikhajlova, Joakim von Wright.

Reasoning About Interactive Systems

• John Derrick, Eerke A. Boiten.

Non-atomic Refinement in Z

• Eric C. R. Hehner, Andrew M. Gravell.

Refinement Semantics and Loop Rules

• Michel R. V. Chaudron, Jan Tretmans, Klaas Wijbrans.

Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System

• Steve King, Jonathan Hammond, Rod Chapman, Andy Pryor.

The Value of Verification: Positive Experience of Industrial Proof

• Anne Elisabeth Haxthausen, Jan Peleska.

Formal Development and Verification of a Distributed Railway Control System

• Kaisa Sere, Elena Troubitsyna.

Safety Analysis in Formal Specification

• Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita.

Formal Specification and Validation of a Vital Communication Protocol

• Herve Marchand, Mazen Samaan.

Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology

• Akira Mori, Kokichi Futatsugi.

Verifying Behavioural Specifications in CafeOBJ Environment

• Razvan Diaconescu, Kokichi Futatsugi, Shusaku Iida.

Component-Based Algebraic Specification and Verification in CafeOBJ

• Shin Nakajima.

Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks

• Manuel Clavel, Fransisco Duran, Steven Eker, Jose Meseguer, Mark-Oliver Stehr.

Maude as a Formal Meta-tool

• Joseph A. Goguen, Grigore Rosu.

Hiding More of Hidden Algebra

• Robert Eschbach.

A Termination Detection Algorithm: Specification and Verification

• Erich Gradel, Marc Spielmann.

Logspace Reducibility via Abstract State Machines

• Martin Dunstan, Tom Kelsey, Ursula Martin, Steve Linton.

Formal Methods for Extensions to CAS

• Rosa M. Jimenez, Fernando Orejas.

An Algebraic Framework for Higher-Order Modules

• Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen.

Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach

• P. Garbett, J. P. Parkes, M. Shackleton, Stuart Anderson.

Secure Synthesis of Code: A Process Improvement Experiment

• Olivier Hainque, Laurent Pautet, Yann Le Biannic, Eric Nassor.

Cronos: A Separate Compilation Toolset for Modular Esterel Applications

Contents

• Samson Abramsky.

Concurrent interaction games

• Richard S. Bird, Jeremy Gibbons, Geraint Jones.

Program optimisation, naturally

• Dines Bjorner.

Domain modelling

• Richard P. Brent.

The binary Euclidean algorithm

• Stephen Brookes.

Communicating Parallel Processes

• Stephen Cameron.

Computing with shapes

• K. Mani Chandy, Michel Charpentier.

Predicate transformers for composition

• Ole-Johan Dahl.

A note on monitor versions

• Edsger W. Dijkstra.

A formula is worth a thousand pictures

• Mike J. C. Gordon.

Linking higher order logic to binary decision diagrams

• David Gries, Fred B. Schneider.

Substitution of equals for equals

• He Jifeng, Xu Qiwen.

Advanced features of the duration calculus

• Eric C. R. Hehner.

Formalism and the variable

• Michael Jackson.

The real world

• Cliff B. Jones.

Compositionality, interference and concurrency

• Donald E. Knuth.

Dancing links

• David May.

The transputer revisited

• Bertrand Meyer.

Principles of language design and evolution

• Robin Milner.

Computing and communication-what's the difference?

• Jayadev Misra.

Generating-functions of interconnection networks

• Carroll Morgan, Annabelle McIver, J. W. Sanders.

Probably Hoare? Hoare probably!

• Roger M. Needham.

Distributed computing: opportunity, challenge, or misfortune?

• C.-H. L. Ong, A. S. Murawski.

A linear-time algorithm for verifying MLL proof nets

• John C. Reynolds.

Intuitionistic reasoning about shared mutable data structure

• A. W. Roscoe, G. M. Reed, R. Forster.

The successes and failures of behavioural models

• J. Michael Spivey, Silvija Seres.

The algebra of searching

• Bernard Sufrin, Oege de Moor.

Modeless structure editing

• Antti Valmari.

A chaos-free failures-divergences semantics

• Niklaus Wirth.

Records, modules, objects, classes, components

• Jim Woodcock, Jim Davies, Christie Bolton.

Abstract data types and processes

• Zhou Chaochen, Dimitar P. Guelev, Zhan Naijun.

A higher-order duration calculus