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 |