| May 17 (Monday) |
| 09:00-09:30 |
Registration |
| 09:30-09:40 |
Opening of IWFMS'2004 |
| 09:40-10:30 |
Invited Talk: Gilles Dowek. Modeling and Verification of an Air Traffic Concept of Operation. |
| 10:30-10:40 |
Break |
| 10:40-11:00 |
Jing Chen. Local model checking real-time value-passing system. |
| 11:00-11:20 |
Wan Fokkink, Jun Pang. Cones and foci for timed transition systems verification revisited |
| 11:20-11:40 |
Coffee Break |
| 11:40-12:30 |
Invited talk: David Nowak. Logical Relations for Monadic Types. |
| 12:30-14:30 |
Lunch Break |
| 14:30-15:20 |
Invited talk: Jean-Jacques Lévy. Confluent calculi for historybased control flow analysis. |
| 15:20-15:30 |
Break |
| 15:30-15:50 |
Chao Qin, Zhong Chen. Using combined method to analyze security protocols. |
| 15:50-16:10 |
Yu Zhang. Extending logical relations for dynamic name creation with encryption. |
| 16:10-16:30 |
Coffee Break |
| 16:30-17:20 |
Invited Talk: James J. Leifer. Language design for distributed computing: Abstraction, Rebinding and Version Control |
| 17:20-17:30 |
Break |
| 17:30-18:30 |
Discussion Time |
| | |
| May 18 (Tuesday) |
| 09:30-10:20 |
Invited Talk: Giuseppe Castagna. Toward a general definition of non-interference for mobile systems. |
| 10:20-10:30 |
Break |
| 10:30-11:20 |
Invited Talk: Guo-Qiang Zhang. Theory and Applications of Formal Concept Analysis. |
| 11:20-11:40 |
Coffee Break |
| 11:40-12:00 |
Sylvain Baro, François Maurel. The qv and qvK calculi: name capture and control. |
| 12:00-12:20 |
Emmanuel Beffara. Realizability with constants. |
| 12:20-12:40 |
Xiao-Cong Zhou. Inserter and categorical model of higher-order subtyping. |
| 12:40-14:30 |
Lunch Break |
| 14:30-14:50 |
Qin Ma, Luc Maranget. Compiling pattern matching in joinpatterns. |
| 14:50-15:10 |
Vicent Simonet. The flow Caml system: information flow analysis in practice. |
| 15:10-15:20 |
Break |
| 15:20-16:10 |
Invited Talk: Jean-François Monin. Formalisation of the Joincalculus in Coq. |
| 16:10-16:40 |
Coffee break |
| 16:40-17:00 |
Shin-ya Nishizaki. Secure execution of client-side scripts by program transformation in an HTTP proxy server. |
| 17:00-17:20 |
Hui Xu, Ai-Min Pan. Formal modeling of event correlation in IDS |
| 17:20-17:30 |
Break |
| 17:30-18:30 |
Invited Talk: Pierre Crégut. Java on Mobile Phones: A New Playground for Formal Methods. |
| | |
| May 19 (Wednesday) |
| 09:30-10:20 |
Invited Talk: Jean-Louis Lanet. The use of Formal Methods in the Smart Card Industry (an experience report) |
| 10:20-10:30 |
Break |
| 10:30-10:50 |
Jens Chr. Godskesen, Thomas Hildebrandt. Copyability types for mobile computing resources. |
| 10:50-11:10 |
Yu-Xin Deng. On mobility and communication. |
| 11:10-11:30 |
Coffee Break |
| 11:30-12:20 |
Invited Talk: Hui-Min Lin. A Predicate Spatial Logic for Mobile Processes. |
| 12:20-14:30 |
Lunch Break |
| 14:30-14:50 |
Pascal Cuoq, Sunae Seo, Hongseok Yang, Kwangkeun Yi. Proof compilation. |
| 14:50-15:10 |
Tao-Lue Chen, Yang-Yue Feng, Jian Lü. Extension of type evolution system for robust mobile ambient. |
| 15:10-15:20 |
Break |
| 15:20-16:10 |
Invited Talk: Ji-Feng He. Linking theories of concurrency |
| 16:10-16:30 |
Coffee break |
| 16:30-17:20 |
Invited Talk: Yu-Xi Fu. On open equivalence. |
| 17:20-18:20 |
Free Time (Discussion) |
| 18:20-18:30 |
Closure |
| | |
| May 20 (Thursday) |
| This day is arranged for an excursion. |