Fourth International Conference on Integrated Formal Methods
4-7 April 2004 in Canterbury, Kent, England
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.
| 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. | |
| 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. | |
| 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)
| 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. | |
| 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. | |
| 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. | |
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)
| 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. | |
