Fifth International Conference on Integrated Formal Methods

29 November - 2 December 2005 in Eindhoven, The Netherlands

Programme

Tuesday, November 29
9:00 - 12:00	Tutorial
Holger Hermanns - QoS Modelling and Analysis for Embedded Systems
12:00 - 13:00	Lunch
13:00 - 17:00	Doctoral symposium
13:00 - 14:00	Session 1
	Building Verification Condition Generators by Compositional Extension
	Arthur van Leeuwen
	Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic
	Peter Höfner
	Linking -calculus and B-Method
	Damien Karkinsky
	Noninterference for sequential and multi-threaded languages
	Thuy Duong Vu
14:00 - 14:15	Break
14:15 - 15:00	Session 2
	Real-time system verification techniques based on abstraction/deduction and model checking
	EunYoung Kang
	Discrete Simulation of Behavioural Hybrid Process Calculus
	Tomas Krilavicius
	Formal Verification of Chi models using PHAVer
	Ka Lok Man, Ramon Schiffelers
15:00 - 15:15	Break
15:15 - 16:00	Session 3
	An Automated Test Generation Process from UML Models to TTCN-3
	Jens Calamé
	Analysis and Implementations of MSC Specifications
	Carsten Kern
	Frameworks based on templates for rigorous model-driven development
	Nuno Amálio
16:00 - 16:15	Break
16:15 - 17:00	Session 4
	A passive Dolev-Yao intruder that reads xor
	Mohammad Torabi Dashti
	Component-Interaction Automata for Specification and Verification of Component Interactions
	Pavlína Vareková, Barbora Zimmerova
	Application of Rewriting Techniques to Verification Problems
	Adam Koprowski
17:00 - 18:30	Welcome reception

Wednesday, November 30
9:00 - 9:10	Conference opening
9:10 - 10:10	Invited talk: FME lecture
David Parnas - A Family of Mathematical Methods for Professional Software Documentation
10:10 - 10:40	Session: Components
Adaptive Techniques for Specification Matching in Embedded Systems: A Comparative Study, Robi Malik and Partha S. Roop
10:40 - 11:00	Coffee break
11:00 - 12:30	Session: State/event-based verification
State/Event Software Verification for Branching-Time Specifications, Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel Ouaknine, Natasha Sharygina, Tayssir Touili and Helmut Veith Exp.Open 2.0: A Flexible tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods, Frederic Lang Chunks: component verification in CSP||B, Steve Schneider, Helen Treharne and Neil Evans
12:30 - 14:00	Lunch
14:00 - 15:30	Session: System development
Agile Formal Method Engineering, Richard Paige and Phil Brooke An Automated Failure Mode and Effect Analysis based on High-Level Design Specification with Behavior Trees, Lars Grunske, Peter Lindsay, Nisansala Yatapanage and Kirsten Winter Enabling Security Testing from Specification to Code, Shane Bracher and Padmanabhan Krishnan
16:00 - 22:00	Excursion and conference dinner

Thursday, December 1
9:30 - 10:30	Invited talk
Doron Peled - Generating Path Conditions for Timed Systems
10:30 - 11:00	Coffee break
11:00 - 12:30	Session: Applications of B
Development of Fault Tolerant Grid Applications Using Distributed B, Pontus Boström and Marina Waldén
Formal methods meet Domain Specific Languages, Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall and Gilles Muller
Synthesizing B Specifications from EB3 Attribute Definitions, Frédéric Gervais, Marc Frappier and Régine Laleau
12:30 - 14:00	Lunch
14:00 - 15:30	Session: Tool support
CZT Support for Z Extensions, Tim Miller, Leo Freitas, Petra Malik and Mark Utting
Embedding the Stable Failures Model of CSP in PVS, Kun Wei and James Heather
Model-based Prototyping of an Interoperability Protocol for Mobile Ad-hoc Networks, Lars Kristensen, Michael Westergaard and Peder Christian Nørgaard
15:30 - 16:00	Coffee break
16:00 - 17:00	Session: Non-software domains
Translating Hardware Process Algebras into Standard Process Algebras -- Illustration with CHP and LOTOS, Gwen Salaun and Wendelin Serwe
Formalising Interactive Voice Services with SDL, Kenneth Turner

Friday, December 2
9:00 - 10:00	Invited talk
Patrice Godefroid - Software Model Checking: Searching for Computations in the Abstract or the Concrete
10:00 - 10:30	Session: Semantics
A Fixpoint Semantics of Event Systems with and without Fairness Assumptions, Hector Ruiz Barradas and Didier Bert
10:30 - 11:00	Coffee break
11:00 - 12:30	Session: UML and statecharts
Consistency Checking of Sequence Diagrams and Statechart Diagrams Using the pi-Calculus, Vitus Lam and Julian Padget
An Integrated Framework for Scenarios and State Machines, Bikram Sengupta and Rance Cleaveland
Consistency in UML and B multi-view specifications, Dieu Donné Okalas Ossami, Jean-Pierre Jacquot and Jeanine Souquières
12:30 - 12:40	Conference closing: BCS-FACS best paper awards
12:40 - 14:00	Lunch
14:00 - 15:00	Doctoral symposium: afterthought

The conference takes place in the Auditorium building. The locations per event are summarized in the following table.

What	Where	When
Lunch breaks	Senaatszaal	All days
Coffee breaks	Voorhof	All days
Tutorial, doctoral symposium	Room 12	Tuesday
IFM presentations	Room 4	Wednesday - Friday
Tool demos	Room 12	Wednesday - Friday
Internet room	Ontvangstzaal 1	All days

All of these locations are quite close together: The main conference room 4 is on the ground level; the conference desk, internet room and lunch/coffee/reception room are on level one; the tutorial/symposium/tool-demo room 12 is on level two.