Fourth International Conference on Integrated Formal Methods

4-7 April 2004 in Canterbury, Kent, England


Programme

Proceedings

Doctoral Symposium

Invited Speakers

Important Dates

Conference Chairs

Program Committee

The Venue

Accommodation Information

Registration

Submission

Contact the Organisers

Pictures


Programme

Day 1 - Sunday, 4 April 2004
Location: Computing Laboratory Octagon
13:00 - 14:00 Registration
14:00 - 15:30 Tutorial (Part I) A Tutorial Introduction to Designs in Unifying Theories of Programming. Jim Woodcock and Ana Cavalcanti.
15:30 - 16:00 Registration + Coffee
16:00 - 17:30 Tutorial (Part II) + FME Meeting(Part I)
17:30 - 19:00 Registration + Welcome Reception
18:30 - 19:00 Doctoral Symposium
19:00 - 19:45 Doctoral Symposium + FME Meeting (Part II)
19:45 - 20:15 Buffet Break
20:15 - 21:00 Doctoral Symposium + FME Meeting (Part II)

Day 2 - Monday, 5 April 2004
Location: Grimond Building
9:00 - 9:15 Registration
9:15 - 9:30 Registration + Opening Session
9:30 - 10:30 FME sponsored invited talk: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. Thomas Ball, Byron Cook, Vladimir Levin, and Sriram K. Rajamani.
10:30 - 11:00 Automating program analysis An Integration of Program Analysis and Automated Theorem Proving. Bill J. Ellis and Andrew Ireland.
11:00 - 11:30 Coffee
11:30 - 13:00 State/event-based verification
Verifying Controlled Components. Steve Schneider and Helen Treharne.
Efficient CSP-Z Data Abstraction. Adalberto Farias, Alexandre Mota, and Augusto Sampaio.
State/Event-based Software Model Checking. Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha.
13:00 - 14:00 Lunch + Tool Demos
14:00 - 15:30 Formalising graphical notations
Formalising Behaviour Trees with CSP. Kirsten Winter.
Generating MSCs from an Integrated Formal Specification Language. Jin Song Dong, Shengchao Qin, and Jun Sun
Object-oriented Modelling with High Level Modular Petri Nets, Cécile Bui Thanh and Hanna Klaudel.
15:30 - 16:00 Coffee
16:00 - 17:30 Refinement
Software Verification with Integrated Data Type Refinement for Integer Arithmetic. Bernhard Beckert and Steffen Schlager
Constituent Elements of a Correctness-Preserving UML Design Approach. Tiberiu Secelaneu and Juha Plosila.
Relating Data Independent Trace Checks in CSP with UNITY Teachability under a Normality Assumption. Xu Wang, A. W. Roscoe, and R. S. Lazic.

Day 3 - Tuesday, 6 April 2004
Location: Grimond Building
9:00 - 10:00 Invited talk: Design Verification for Control Engineering. Ursula Martin.
10:00 - 10:30 Object orientation Linking CSP-OZ with UML and Java: A Case Study. Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim.
10:30 - 11:00 Coffee
11:00 - 12:30 Object orientation
UML to B: Formal Verification of Object-oriented Models. K. Lano, D. Clark and K. Androutsopoulos.
Specification and Verification of Synchronizing Concurrent Objects. Gabriel Ciobanu and Dorel Lucanu.
Understanding Object-Z Operations as Generalised Substitutions Steve Dunne.
12:30 - 13:30 Lunch + Tool Demos
13:30 - 15:00 Hybrid and timed automata
Embeddings of Hybrid Automata in Process Algebra. Tim A. C. Willemse.
An Optimal Approach to Hardware/Software Partitioning for Synchronous Model. Pu Geguang, Dang Van Hung, He Jifeng, and Wang Yi.
A Many-valued Logic with Imperative Semantics for Incremental Specification of Timed Models. Ana Fernández Vilas, José J. Pazos Arias, Rebeca P. Diáz Redondo, Alberto Gil Solla and Jorge García Duque.
15:00 - 15:30 Coffee
15:30 - 17:00 Integration frameworks
Integrating Temporal Logics. Yifeng Chen and Zhiming Liu
Integration of Specification Languages using Viewpoints. Marius C. Bujorianu.
Integrating Formal Methods by Unifying Abstractions. Raymond Boute.
19:00 Conference Banquet (Departure at 17:40)

Day 4 - Wednesday, 7 April 2004
Location: Grimond Building
9:30 - 10:30 Invited talk: Integrating Model Checking and Theorem Proving in a Reflective Functional Language. Tom Melham.
10:30 - 11:00 Verifying interactive systems Formally Justifying User-centred Design Rules: a Case Study on Post-completion Errors. Paul Curzon and Ann Blandford
11:00 - 11:30 Coffee
11:30 - 12:30 Testing and assertions
Using UML Sequence Diagrams as the Basis for a Formal Test Description Language. Simon Pickin and Jean-Marc Jézéquel.
Viewpoint-based Testing of Concurrent Components. Luke Wildman, Roger Duke, and Paul Strooper.
12:30 - 13:00 Closing Session + BCS-FACS Best Paper Award
13:00 - 14:00 Lunch (Eliot; doctoral symposium participants: evaluation in Grimond Seminar Room 3)

Fortest Meeting

Wednesday, 7 April 2004
Location: Computing Laboratory - SW102
14:30 - 15:00 Observability in the distributed test architecture. Rob Hierons (joint work with Prof. Hasan Ural, University of Ottawa)
15:00 - 15:30 Validity of Test Oracles and Semantics of Algebraic Specifications. Hong Zhu
15:30 - 15:45 Coffee
15:45 - 16:15 Testing ROOMcharts with Conditional Properties. Christopher Robinson-Mallett
16:15 - 16:40 On the Relationship Between Two Control-Flow Coverage Criteria: 'All JJ-Paths' and MCDC. Martin Woodward
16:40 - 17:40 Fortest Business Meeting


Go to the University of Kent's Home Page Hosted by Computer Science @ Kent This page is maintained by Marcel Oliveira.