20-24/09/99  - Toulouse - France

Technical Symposium  Programme

 Opening Session and Welcome (9.00 am)

Keynote speaker: C.A.R Hoare
"Theories of programming: top-down and bottom-up and meeting in the middle"

Session 1A Software Architectures
"Refinement of Pipe and Filter Architectures"
Jan Philipps & Bernhard Rumpe

"A Formalization of Software Architecture"
John Herbert, Bruno Dutertre, Robert Riemenschneider, & Victoria Stavridou

Session 1B Programming Concepts
"Component and Interface Refinement in Closed-system Specifications"
Reino Kurki-Suoni

"Semantics of first order parametric specifications"
Dusko Pavlovic

Session 1C Safety
"Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System"
Michel Chaudron, Jan Tretmans, & Klaas Wijbrans

"The Value of Verification: Positive Experience of Industrial Proof"
Steve King, Jonathan Hammond, Rod Chapman, & Andy Pryor

Session 2A 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 & Pierre Lartigue

"Meteor: A Successful Application of B in a Large Project"
Patrick Behm, Paul Benoit, Alain Faivre, & Jean-Marc Meynadier

"Formal Development of Databases in ASSO and B"
Brian Matthews & Elvira Locuratolo

Session 2B Model Checking
"A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software"
Yonit Kesten, Amit Klein, Amir Pnueli, & Gil Raanan

"Error Detection with Directed Symbolic Model checking"
Frank Reffel & Stefan Edelkamp

"Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multirobot Coordination"
R. Alur, J. Esposito, M. Kim, V. Kumar, & I. Lee

Session 2C Composition and Synthesis
"Bunches for Object-Oriented, Concurrent, and Real-Time Specification"
Richard Paige & Eric C.R. Hehner

"Applications of structural synthesis of programs"
Enn Tyugu, Mihhail Matskin, & Jaan Penjam

"Towards a Compositional Approach to the Design and Verification of Distributed Systems"
Michel Charpentier & K. Mani Chandy
 

Session 3A Telecommunications
"Formal Modeling in a Commercial Setting: A Case Study"
Andre Wong & Marsha Chechik

"KVEST: Automated Generation of Test Suites from Formal Specifications"
Igor Burdonov, Alexander Kossatchev, Alexander Petrenko, & Dmitri Galter,

"Feature Interaction Detection using Testing and Model-checking Experience report"
Lydie du Bousquet

Session 3B Object Orientation
"Developing BON as an Industrial-Strength Formal Method"
Richard F. Paige & Jonathan Ostroff

"On the Expressive Power of OCL"
Maria Victoria Cengarle

"A Systematic Approach to transform OMT diagrams to a B specification"
Eric Meyer & Jeanine Souquières

Session 3C Security
"Secure Interoperation of Secure Distributed Databases: an Architecture Verification Case Study"
Fred Gilham, R.A. Riemenschneider, & Victoria Stavridou

"A Formal Security Model for Microprocessor Hardware"
Volkmar Lotz, Volker Kessler, & Georg Walter

"Abstraction and testing"
Steve Schneider

Invited speaker: Cliff B. Jones
"Scientific decisions which Characterize VDM: a personal view"

Session 4A Testing
"Verifying Consistency and Validity of Formal Specifications by Testing"
Shaoying Liu

"A GSM-MAP Protocol Experiment Using Passive Testing"
Marine Tabourier, Ana Cavalli, & Melania Ionescu

Session 4B Programming Concepts
"From Informal Requirements to COOP: a Concurrent Automata Approach"
Pascal Poizat, Christine Choppy, & Jean-Claude Royer

"A Framework for Defining Object-Calculi"
Frederic Lang, Pierre Lescanne, & Luigi Liquori

Session 4C Discussion Session: Industrial Experiences

Session 4D Discussion Session: Education, Tools and Techniques

Session 5A Telecommunications
"Emma: Developing an Industrial Reachability Analyser for SDL"
Nisse Husberg & Tapio Manner

"Correction Proof of the Standardized Algorithm for ABR Conformance"
Jean-Francois Monin & Francis Klay

"Verifying a Distributed Database Lookup Manager Written in Erlang"
Thomas Arts & Mads Dam

Session 5B ETAPS
"A Translation of Statecharts to Esterel"
A.K. Bhattacharjee, S.D. Dhodapk au Sanjit Seshia, & R.K. Shyamasundar

"An Operational Semantics for Timed RAISE"
Xia Yong & Chris Georg

"Data Abstraction for CSP-OZ"
Heike Wehrheim

Session 5C Program Verification
"On Excusable and Inexcusable Failures: Looking for an Adequate Notion of Translation Correctness"
Markus Muller-Olm & Andreas Wolf

"Towards Tool Support for Program Verification and Construction"
Richard Verhoeven & Roland Backhouse

"Software verification based on linear programming"
S. Dellacherie, S. Devulder, & J-L. Lambert

Session 6A Programming Concepts
"A more complete TLA"
Stephan 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"
Andrew Martin

Session 6B ETAPS
"Systems Development using Z Generics"
Fiona Polack & Susan Stepney

"A Brief Summary of VSPEC"
Perry Alexander, Murali Rangarajan, & Phillip Baraona

"Enhancing the Pre- and Postcondition Technique for More Expressive Specifications"
Gary T. Leavens & Albert L. Baker

Session 6C Integration of notations and techniques
"Sensors and Actuators in TCOZ"
Brendan Mahony & Jin Song Dong

"The UniForM Workbench, a Universal Development Environment for Formal Methods"
Bernd Krieg-Bruckner, Jan Peleska, Ernst-Rudiger Olderog, & Alexander Baer

"Integrating Formal Description Techniques"
Bernard Schätz & Franz Huber

Invited speaker: Amir Pnueli

Session 7A Safety
"Formal Development and Verification of a Distributed Railway Control System"
Anne Haxthausen & Jan Peleska

"Hazard Analysis in Formal Specification"
Kaisa Sere & Elena Troubitsyna

"Formal Specification and Validation of a Vital Communication Protocol"
A. Cimatti, P.L. Pieraccini, R. Sebastiani, P. Traverso, & A. Villafiorita

"On the Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology"
H. Marchand & M. Samaan

Session 7B Refinement
"A Weakest Precondition Semantics for Refinement in an Object-Oriented Language"
Ana Cavalcanti & David A. Naumann

"Reasoning About Interactive Systems"
Ralph Back, Anna Mikhajlova, & Joakim von Wright

"Non-atomic refinement in Z"
John Derrick & Eerke Boiten

"Refinement Semantics and Loop Rules"
Eric C.R. Hehner & Andrew H. Gravell

Session 7C Open Information Systems
"Formal Modeling of the Enterprise JavaBeans Component Integration Framework"
Joao Pedro Sousa & David Garlan

"Developing Components in Presence of Re-entrance"
Leonid Mikhajlov, Emil Sekerinski, & Linas Laibinis

"Communication and Synchronisation using Interaction Objects"
H.B.M. Jonkers

"Modelling Microsoft COM using pi-Calculus"
Loe M.G. Feijs

Invited speaker: John Rushby
"Mechanized Formal Methods: Where Next"

Session 8A FM into the System Development Process
"Formal Design for Automatic Coding and testing: The ESSI/SPACES Project"
Eric Conquet & Jean-Luc Marty

"A Business Process Design Language"
Henk Eertink, Wil Janssen, Paul Oude Luttighuis, Wouter Teeuw, & Chris Vissers

Session 8B OBJ
"Verifying Behavioural Specifications in CafeOBJ Environment"
Akira Mori & Kokichi Futatsugi

"Component-based Algebraic Specification and Verification in CafeOBJ"
Razvan Diaconescu, Kokichi Futatsugi, & Shusaku Iida

Session 8C Discussion Session: Industrial Experiences

Session 8D Discussion Session: Formalisms

Session 9A The B-Method
"Interpreting the B-Method in the Refinement Calculus"
Yann Rouzaud

"Compositional Symmetric Sharing in B"
Martin Buchi & Ralph Back

"Structural Embeddings: Mechanization with Method"
Cesar Munoz & John Rushby

Session 9B Model Checking
"Symbolic Model Checking with Fewer Fixpoint Computations"
David Deharbe & Anamaria Martins Moreira

"On-the-fly Verification of Linear Temporal Logic"
Jean-Michel Couvreur

"On-The-Fly Controller Synthesis for Discrete and Dense-Time Systems"
Stavros Tripakis & Karine Altisen

Session 9C OBJ
"Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks"
Shin Nakajima

"Maude as a Formal Meta-Tool"
M. Clavel, F.Duran, S. Eker, & Jose Meseguer

"Hiding More of Hidden Algebra"
Joseph Goguen & Grigore Rosu

Invited Speaker: Joseph Sifakis
"Integration, the Price of Success"

Invited Speaker: Michael A. Jackson
"The Role of Formalism in Method"

Session 10 A Security
"Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol"
Dan Zhou & Shiu-Kai Chin

"Probabilistic Polynomial-time Equivalence and Security Protocols"
P. Lincoln, J.Mitchell, M. Mitchell, & A.Scedrov

"A Uniform Approach for the Definition of Security Properties"
Riccardo Focardi & Fabio Martinelli

"Group Principals and the Formalization of Anonymity"
Paul F. Syverson & Stuart G. Stubblebine

Session 10 B ASM + AMAST
"A Termination Detection Algorithm: Specification and Verification"
Robert Eschbach

"Logspace Reducibility via Abstract State Machines"
Erich Grädel & Marc Spielmann

"Formal Methods for Extensions to CAS"
Martin N. Dunstan, Tom Kelsey, Ursula Martin, & Steve Linton

"An Algebraic Framework for Higher-Order Modules"
Rosa Jimenez & Fernando Orejas

Session 10 C Co-design
"Validation of Mixed Signal Alpha Real Time Systems through Affine Calculus on Clock Synchronisation Constraints"
Irina M. Smarandache & Thierry Gautier

"Combining Theorem Proving and Continuous Models in Synchronous Design"
Simin Nadjm-Tehrani & Ove Akerlund

"ParTS: A partitioning transformation system"
Juliano Iyoda, Augusto Sampaio, & Leila Silva

"A Behavioral Model for Co-design"
He Jifeng

Session 11A The B-Method
"The Safe Machine: a new specification construct for B"
Steve Dunne

"csp2B: A Practical Approach to Combining CSP and B"
Michael Butler

"Test Criteria Definition for B Models"
Salimeh Behnia & Helene Waeselynck

Session 11 B Model Checking
"Formula based Abstractions of Transition Systems for Real-time Model Checking"
Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, & Gigliona Vaglini

"IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems"
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krim, & Laurent Mounier

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

Session 11C Avionics
"Applying formal proof techniques to avionics software: a pragmatic approach"
Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, & Dominique 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"
Olivier Hainque, Laurent Pautet, Yann Le Biannic, & Eric Nassor

Updated June 14th