FME 2001: Berlin, Germany

José Nuno Oliveira, Pamela Zave (Eds.): FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings. Lecture Notes in Computer Science 2021 Springer 2001, ISBN 3-540-41791-5

Invited Talk

Daniel Jackson:
Lightweight Formal Methods. 1

Proof and Model-checking

Françoise Bellegarde, Christophe Darlot, Jacques Julliand, Olga Kouchnarenko:
Reformulation: A Way to Combine Dynamic Properties and B Refinement. 2-19
Steffen Helke, Thomas Santen:
Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries. 20-42
Joseph E. Stoy, Xiaowei Shen, Arvind:
Proofs of Correctness of Cache-Coherence Protocols. 43-71

Model Checking

Marsha Chechik, Steve M. Easterbrook, Victor Petrovykh:
Model-Checking over Multi-valued Logics. 72-98
Michael Leuschel, Thierry Massart, Andrew Currie:
How to Make FDR Spin LTL Model Checking of CSP by Refinement. 99-118
Fabrice Derepas, Paul Gastin, David Plainfossé:
Avoiding State Explosion for Distributed Systems with Timestamps. 119-134

Security

Jan Jürjens:
Secrecy-Preserving Refinement. 135-152
Heiko Mantel:
Information Flow Control and Applications - Bridging a Gap. 153-172

Agent Architectures

Vangalur S. Alagar, Zheng Xi:
A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures. 173-196
Nalini Venkatasubramanian, Carolyn L. Talcott, Gul Agha:
A Formal Model for Reasoning about Adaptive QoS-Enabled Middleware. 197-221

Invited Talk

Jayadev Misra:
A Programming Model for Wide-Area Computing. 222

Object-Oriented Formal Modelling

Andres Flores, Richard Moore, Luis Reynoso:
A Formal Model of Object-Oriented Design and GoF Design Patterns. 223-241
Sophie Dupuy-Chessa, Lydie du Bousquet:
Validation of UML Models Thanks to Z and Lustre. 242-258
Claus Pahl:
Components, Contracts, and Connectors for the Unified Modelling Language UML. 259-277

Real Time Systems

Adnan Sherif, Augusto Sampaio, Sérgio Cavalcante:
An Integrated Approach to Specification and Validation of Real-Time Systems. 278-299
Stephen Paynter:
Real-Time Logic Revisited. 300-317
Dirk Beyer:
Improvements in BDD-Based Reachability Analysis of Timed Automata. 318-343

Concurrency and Parallelism

Leila Silva, Augusto Sampaio, Geraint Jones:
Serialising Parallel Processes in a Hardware/Software Partitioning Context. 344-363
Jonathan Burton, Maciej Koutny, Giuseppe Pappalardo:
Verifying Implementation Relations. 364-383

Logic and Foundations

Muffy Calder, Savi Maharaj, Carron Shankland:
An Adequate Logic for Full LOTOS. 384-395
Mícheál Mac an Airchinnigh:
Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics. 396-418
Shmuel Katz:
Faithful Translations among Models and Specifications. 419-434

Invited Talk

Simon L. Peyton Jones:
Composing Contracts: An Adventure in Financial Engineering. 435

Formal Techniques in System Testing

Manuel J. Fernández Iglesias, Francisco J. González-Castaño, José M. Pousada Carballo, Martín Llamas Nistal, Alberto Romero Feijoo:
From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study. 436-448
Laurent Arditi, Hédi Boufaïed, Arnaud Cavanié, Vincent Stehlé:
Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP System. 449-464
Odile Laurent, Pierre Michel, Virginie Wiels:
Using Formal Verification Techniques to Reduce Simulation and Test Effort. 465-477

Case Studies, Tools and Verification Experiments

Pieter H. Hartel, Michael J. Butler, Eduard de Jong, Mark Longley:
Transacted Memory for Smart Cards. 478-499
Cormac Flanagan, K. Rustan M. Leino:
Houdini, an Annotation Assistant for ESC/Java. 500-517
Dragan Bosnacki, Dennis Dams, Leszek Holenderski:
A Heuristic for Symmetry Reductions with Scalarsets. 518-533

Information Maintenance and Refactoring

Michael Johnson, Robert D. Rosebrugh:
View Updatability Based on the Models of a Formal Specification. 534-549
Ralf Lämmel:
Grammar Adaptation. 550-570

Combining Strategies

Bernhard K. Aichernig:
Test-Case Calculation through Abstraction. 571-589
Marielle Doche, Isabelle Vernier-Mounier, Fabrice Kordon:
A Modular Approach to the Specification and Validation of an Electrical Flight Control System. 590-610
Natasha Sharygina, Doron Peled:
A Combined Testing and Verification Approach for Software Reliability. 611-628