24th IFIP WG 6.1 International Conference on
Formal Techniques for Networked and
Distributed Systems
FORTE 2004
27-30 September, 2004, Madrid, Spain
| Monday September 27th | Tuesday September 28th | Wednesday September 29th | Thursday September 30th |
|---|---|---|---|
|
Tutorials I-II Tutorial I: Roberto Gorrieri Tutorial II: Farn Wang |
Conference Opening | Invited Talk Tommaso Bolognesi |
Invited Talk Juan Quemada |
| Invited Talk Martin Abadi | |||
| Coffee Break | |||
|
Tutorials II-I Tutorial I: Roberto Gorrieri. Tutorial II: Farn Wang |
Session II Automata at Work |
Session V Verification I |
Session VIII Verification II |
| Conference Closing | |||
| Lunch | |||
| Session I FDL at Work |
Session III Testing |
Session VI Petri Nets |
Transfer to Toledo for colocated workshops |
| Guided Tour | Coffee Break | ||
| Session IV Formal Methods for Distributed Systems |
Session VII Work in Progress | ||
| PC Meeting/Dinner | Conference Dinner | ||
Tutorial I: Roberto Gorrieri. Foundations of Security Analysis and Design
Tutorial II: Farn Wang. Symbolic Techniques for the verification of real-time and embedded systems with BDD-like data structures
Application of FDL
Parameterized Models for Distributed Java Objects. Eric Madelaine, Rabéa Boulifa, Tomas Barros - INRIA.
Towards the Harmonisation of UML and SDL. Rüdiger Grammes, Reinhard Gotzhein - Technical University of Kaiserslautern.
Localizing Program Errors for Cimple Debugging. Samik Basu - Iowa State University; Diptikalyan Saha, Scott Smolka - State University of New York at Stony Brook.
Application of Automata
Formal Verfication of a Practical Lock-Free Queue Algorithm. Simon Doherty, Lindsay Groves - Victoria University of Wellington; Victor Luchangco, Mark Moir - Sun Microsystems Laboratories.
Formal Verification of Web Applications Modeled by Communicating Automata. May Haydar, Alexandre Petrenko - CRIM, Centre de recherche informatique de Montréal; Houari Sahraoui - Université de Montréal.
Towards Design Recovery from Observations. Hasan Ural - University Of Ottawa, Husnu Yenigun - Sabanci University.
Testing Session
Network Protocol System Passive Testing for Fault Management - a Backward Checking Approach. Baptiste Alcalde, Ana Cavalli, Davy Khuu - GET-INT; Dongluo Chen - Tsinghua University, David Lee - Bell Labs Research.
Connectivity Testing through Model-Checking. Jens Chr. Godskesen - Center of Embedded Software Systems and IT-University; Brian Nielsen, Arne Skou - Center of Embedded Software Systems.
Fault Propagation by Equation Solving. Khaled El-Fakih - American University of Sharjah, Nina Yevtushenko - Tomsk State University.
Distributed Systems Session.
Automatic Generation of the Run-Time Test Oracles for Distributed Real-Time Systems. Xin Wang, Ji Wang, ZhiChang Qi - National Laboratory for Parallel and Distributed Processing.
Formal Composition of Distributed Scenario. Aziz Salah - Univ of Quebec at Montreal; Rabeb Mizouni, Rachida Dssouli - Concordia Univ.
Conditions for Resolving Observability Problems in Distributed Testing. Jessica Chen - School of Computer Science, University of Windsor; Robert Hierons - Brunel University, Hasan Ural - University of Ottawa.
Verification Session
Integrating Formal Verification with Murphi of Distributed Cache Coherence Protocols in FAME Multiprocessor System Design. Ghassan Chehaibar - Bull, Platforms Hardware R∧D.
Witness and Counterexample Automata for ACTL. Robert Meolic - University of Maribor, Alessandro Fantechi - DSI - Univ. di Firenze, Stefania Gnesi - ISTI - CNR.
A Symbolic Symbolic State-Space Representation. Yann Thierry-Mieg, Jean-Michel Ilié, Denis Poitrenaud - Laboratoire d'Informatique de Paris 6.
Petri Nets Session
Introducing the iteration in sPBC. Hermenegilda Macia, Valentin Valero, Diego Cazorla, Fernando Cuartero - Universidad de Castilla-La Mancha.
Petri net semantics of the finite pi-calculus. Raymond Devillers - Université Libre de Bruxelles, Hanna Klaudel - Université d'Évry, Maciej Koutny - University of Newcastle upon Tyne.
Symbolic Diagnosis of Partially Observable Concurrent Systems. Thomas CHATAIN, Claude JARD - IRISA/ENS Cachan.
Work in progress Session.
Systematic Functional Design of an XML Editor. Hannes Verlinde, Raymond Boute - Ghent University
A Framework for Time in FDTs. Susanne Graf - Verimag, Andreas Prinz - Agder University College
Automated Verification of Features with Situation Calculus. Pascal Urso, Pierre-Yves Schobbens - Facultés Universitaires Notre-Dame de la Paix
A Methodology for Policy Conflict Detection Using Model Checking Techniques. Peter H. Deussen, Ina Schieferdecker, - Fraunhofer Research Institute, Hiroaki Kamoda - NTT Data Corporation
Generating Interoperability Test Cases from Conformance Test Case Generation Tools. Ismail Berrada, Richard Castanet, Patrick Félix, Ousmane Koné - Université Bordeaux 1
Verification Session
Automatized verification of ad hoc routing protocols. Oskar Wibling, Joachim Parrow, Arnold Pears - Uppsala University.
A Temporal Logic Based Framework for Intrusion Detection. Prasad Naldurg, Koushik Sen, Prasanna Thati - University of Illinois at Urbana Champaign.
Transfer to Toledo (Colocated workshops).