| Foundations of System Specification (IFIP WG 1.3) |
| From Informal Requirements to COOP: A Concurrent Automata Approach / P. Poizat ; C. Choppy ; J.-C. Royer |
| A Framework for Defining Object-Calculi / F. Lang ; P. Lescanne ; L. Liquori |
| European Theory and Practice of Software (ETAPS) |
| A Translation of Statecharts to Esterel / S. A. Seshia ; R. K. Shyamasundar ; A. K. Bhattacharjee ; S. D. Dhodapkar |
| An Operational Semantics for Timed RAISE / X. Yong ; C. George |
| Data Abstraction for CSP-OZ / H. Wehrheim |
| Systems Development Using Z Generics / F. Polack ; S. Stepney |
| A Brief Summary of VSPEC / P. Alexander ; M. Rangarajan ; P. Baraona |
| Enhancing the Pre- and Postcondition Technique for More ExpressiveSpecifications / G. T. Leavens ; A. L. Baker |
| Program Verification |
| On Excusable and Inexcusable Failures / M. Müller-Olm ; A. Wolf |
| Interfacing Program Construction and Verification / R. Verhoeven ; R. Backhouse |
| Software Verification Based on Linear Programming / S. Dellacherie ; S. Devulder ; J.-L. Lambert |
| Integration of Notation and Techniques |
| Sensors and Actuators in TCOZ / B. Mahony ; J. S. Dong |
| The UniForM Workbench, a Universal Development Environment for Formal Methods / B. Krieg-Brückner ; J. Peleska ; E.-R. Olderog ; A. Baer |
| Integrating Formal Description Techniques / B. Schätz ; F. Huber |
| Formal Description of Programming Concepts (IFIP WG 2.2) |
| A More Complete TLA / S. Merz |
| Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach / F. S. de Boer ; U. Hannemann ; W.-P. de Roever |
| Relating Z and First-Order Logic / A. Martin |
| Open Information Systems |
| Formal Modeling of the Enterprise JavaBeansTM Component Integration Framework / J. P. Sousa ; D. Garlan |
| Developing Components in the Presence of Re-entrance / L. Mikhajlov ; E. Sekerinski ; L. Laibinis |
| Communication and Synchronisation Using Interaction Objects / H. B. M. Jonkers |
| Modelling Microsoft COM Using π-Calculus / L. M. G. Feijs |
| Co-design |
| Validation of Mixed Signal-Alpha Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints / I. M. Smarandache ; T. Gautier ; P. Le Guernic |
| Combining Theorem Proving and Continuous Models in Synchronous Design / S. Nadjm-Tehrani ; O. Åkerlund |
| ParTS: A Partitioning Transformation System / J. Iyoda ; A. Sampaio ; L. Silva |
| A Behavioral Model for Co-design / J. He |
| Refinement |
| A Weakest Precondition Semantics for an Object-Oriented Language of Refinement / A. Cavalcanti ; D. A. Naumann |
| Reasoning About Interactive Systems / R. Back ; A. Mikhajlova ; J. von Wright |
| Non-atomic Refinement in Z / J. Derrick ; E. Boiten |
| Refinement Semantics and Loop Rules / E. C. R. Hehner ; A. M. Gravell |
| Safety |
| Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System / M. Chaudron ; J. Tretmans ; K. Wijbrans |
| The Value of Verification: Positive Experience of Industrial Proof / S. King ; J. Hammond ; R. Chapman ; A. Pryor |
| Formal Development and Verification of a Distributed Railway Control System / A. E. Haxthausen |
| Safety Analysis in Formal Specification / K. Sere ; E. Troubitsyna |
| Formal Specification and Validation of a Vital Communication Protocol / A. Cimatti ; P. L. Pieraccini ; R. Sebastiani ; P. Traverso ; A. Villafiorita |
| Incremental Design of a Power Transformer Station Controller Using aController Synthesis Methodology / H. Marchand ; M. Samaan |
| OBJ/Cafe OBJ/Maude |
| Verifying Behavioural Specifications in CafeOBJ Environment / A. Mori ; K. Futatsugi |
| Component-Based Algebraic Specification and Verification in CafeOBJ / R. Diaconescu ; S. Iida |
| Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks / S. Nakajima |
| Maude as a Formal Meta-tool / M. Clavel ; F. Durán ; S. Eker ; J. Meseguer ; M.-O. Stehr |
| Hiding More of Hidden Algebra / J. Goguen ; G. Roşu |
| Abstract State Machines (ASM) and Algebraic Methods in Software Technology (AMAST) |
| A Termination Detection Algorithm: Specification and Verification / R. Eschbach |
| Logspace Reducibility via Abstract State Machines / E. Grädel ; M. Spielmann |
| Formal Methods for Extensions to CAS / M. N. Dunstan ; T. Kelsey ; U. Martin ; S. Linton |
| An Algebraic Framework for Higher-Order Modules / R. Jiménez ; F. Orejas |
| Avionics |
| Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach / F. Randimbivololona ; J. Souyris ; P. Baudin ; A. Pacalet ; J. Raguideau ; D. Schoen |
| Secure Synthesis of Code: A Process Improvement Experiment / P. Garbett ; J. P. Parkes ; M. Shackleton ; S. Anderson |
| Cronos: A Separate Compilation Toolset for Modular Esterel Applications / O. Hainque ; L. Pautet ; Y. Le Biannic ; É. Nassor |
| Works-in-Progress |
| Tool Support for Production Use of Formal Techniques / J. C. Knight ; P. T. Fletcher ; B. R. Hicks |
| Modeling Aircraft Mission Computer Task Rates / B. P. Mahony ; N. Fulton |
| A Study of Collaborative Work: Answers to a Test on Formal Specification in B / H. Habrias ; J.-Y. Lafaye |
| Archived Design Steps in Temporal Logic / P. Kellomäki ; T. Mikkonen |
| A PVS-Based Approach for Teaching Constructing Correct Iterations / M. Lévy ; L. Trilling |
| A Minimal Framework for Specification Theory / B. Baumgarten |
| A Model of Specification-Based Testing of Interactive Systems / I. MacColl ; D. Carrington |
| Algebraic Aspects of the Mapping between Abstract Syntax Notation One and CORBA IDL / R. Ocică ; D. lonescu |
| Retrenchment / R. Banach ; M. Poppleton |
| Proof Preservation in Component Generalization / A. M. Moreira |
| Industrial Experience |
| Formal Modelling and Simulation of Train Control Systems Using Petri Nets / M. Meyer zu Hörste ; E. Schnieder |
| Formal Specification of a Voice Communication System Used in Air Traffic Control / J. Hörl ; B. K. Aichernig |
| Model-Checking the Architectural Design of a Fail-Safe Communication System for Railway Interlocking Systems / B. Buth ; M. Schrönen |
| Analyzing the Requirements of an Access Control Using VDMTools and PVS / G. Droschl |
| Cache Coherence Verification with TLA+ / H. Akhiani ; D. Doligez ; P. Harter ; L. Lamport ; J. Scheid ; M. Tuttle ; Y. Yu |
| Author Index |
| Invited Papers |
| Theories of Programming: Top-Down and Bottom-Up Meeting in the Middle / C. A. R. Hoare |
| Scientific Decisions which Characterise VDM / C. B. Jones |
| Mechanized Formal Methods: Where Next? / J. Rushby |
| Integration, the Price of Success / J. Sifakis |
| The Role of Formalism in Method / M. Jackson |
| Integration into the Development Process |
| Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project / E. Conquet ; J.-L. Marty |
| A Business Process Design Language / H. Eertink ; W. Janssen ; P. O. Luttighuis ; W. Teeuw ; C. Vissers |
| Software Architecture |
| Refinement of Pipe-and-Filter Architectures / J. Philipps ; B. Rumpe |
| A Formalization of Software Architecture / J. Herbert ; B. Dutertre ; R. Riemenschneider ; V. Stavridou |
| European Association for Theoretical Computer Science (EATCS) |
| Component and Interface Refinement in Closed-System Specifications / R. Kurki-Suonio |
| Semantics of First Order Parametric Specifications / D. Pavlović |
| Model Checking |
| A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software / Y. Kesten ; A. Klein ; A. Pnueli ; G. Raanan |
| Error Detection with Directed Symbolic Model Checking / F. Reffel ; S. Edelkamp |
| Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination / R. Alur ; J. Esposito ; M. Kim ; V. Kumar ; I. Lee |
| On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems / S. Tripakis ; K. Altisen |
| On-the-Fly Verification of Linear Temporal Logic / J.-M. Couvreur |
| Symbolic Model Checking with Fewer Fixpoint Computations / D. Déharbe |
| Formula Based Abstractions of Transition Systems for Real-Time Model Checking / R. Barbuti ; N. De Francesco ; A. Santone ; G. Vaglini |
| IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems / M. Bozga ; J.-C. Fernandez ; L. Ghirvu ; S. Graf ; J.-P. Krimm ; L. Mounier |
| Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes / F. Wang |
| The B Method |
| The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications / D. Sabatier ; P. Lartigue |
| Météor: A Successful Application of B in a Large Project / P. Behm ; P. Benoit ; A. Faivre ; J.-M. Meynadier |
| Formal Development of Databases in ASSO and B / B. Matthews ; E. Locuratolo |
| Interpreting the B-Method in the Refinement Calculus / Y. Rouzaud |
| Compositional Symmetric Sharing in B / M. Büchi |
| Structural Embeddings: Mechanization with Method / C. Muñoz |
| The Safe Machine: A New Specification Construct for B / S. Dunne |
| csp2B: A Practical Approach to Combining CSP and B / M. Butler-Test Criteria Definition for B Models ; S. Behnia ; H. Waeselynck |
| Composition and Synthesis |
| Bunches for Object-Oriented, Concurrent, and Real-Time Specification / R. F. Paige |
| Applications of Structural Synthesis of Programs / E. Tyugu ; M. Matskin ; J. Penjam |
| Towards a Compositional Approach to the Design and Verification of Distributed Systems / M. Charpentier ; K. M. Chandy |
| Telecommunications |
| Formal Modeling in a Commercial Setting: A Case Study / A. Wong ; M. Chechik |
| KVEST: Automated Generation of Test Suites from Formal Specifications / I. Burdonov ; A. Kossatchev ; A. Petrenko ; D. Gaiter |
| Feature Interaction Detection Using Testing and Model-Checking Experience Report / L. du Bousquet |
| Emma: Developing an Industrial Reachability Analyser for SDL / N. Husberg ; T. Manner |
| Correction Proof of the Standardized Algorithm for ABR Conformance / J.-F. Monin ; F. Klay |
| Verifying a Distributed Database Lookup Manager Written in Erlang / T. Arts ; M. Dam |
| Security |
| Secure Interoperation of Secure Distributed Databases / F. Gilham ; R. A. Riemenschneider |
| A Formal Security Model for Microprocessor Hardware / V. Lotz ; V. Kessler ; G. Walter |
| Abstraction and Testing / S. Schneider |
| Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol / D. Zhou ; S.-K. Chin |
| Probabilistic Polynomial-Time Equivalence and Security Analysis / P. Lincoln ; J. Mitchell ; M. Mitchell ; A. Scedrov |
| A Uniform Approach for the Definition of Security Properties / R. Focardi ; F. Martinelli |
| Group Principals and the Formalization of Anonymity / P. F. Syverson ; S. G. Stubblebine |
| Object-Orientation |
| Developing BON as an Industrial-Strength Formal Method / J. S. Ostroff |
| On the Expressive Power of OCL / L. Mandel ; M. V. Cengarle |
| A Systematic Approach to Transform OMT Diagrams to a B Specification / E. Meyer ; J. Souquières |
| Testing |
| Verifying Consistency and Validity of Formal Specifications by Testing / S. Liu |
| A GSM-MAP Protocol Experiment Using Passive Testing / M. Tabourier ; A. Cavalli ; M. Ionescu |
| Test Criteria Definition for B Models / M. Butler |
| A Systematic Approach to Transform OMT Diagrams to a B specification |
| Enhancing the Pre- and Postcondition Technique for More Expressive Specifications |
| Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology / S. Devülder ; andA. Villafiorita |
| Analyzing the Requirements of an Access Control Using VDMToolsand PVS / D. Ionescu |
| Foundations of System Specification (IFIP WG 1.3) |
| From Informal Requirements to COOP: A Concurrent Automata Approach / P. Poizat ; C. Choppy ; J.-C. Royer |
| A Framework for Defining Object-Calculi / F. Lang ; P. Lescanne ; L. Liquori |
| European Theory and Practice of Software (ETAPS) |
| A Translation of Statecharts to Esterel / S. A. Seshia ; R. K. Shyamasundar ; A. K. Bhattacharjee ; S. D. Dhodapkar |
| An Operational Semantics for Timed RAISE / X. Yong ; C. George |
