4. IFM 2004: Canterbury, Kent, England

@proceedings{DBLP:conf/ifm/2004,
  editor    = {Eerke A. Boiten and
               John Derrick and
               Graeme Smith},
  title     = {Integrated Formal Methods, 4th International Conference, IFM
               2004, Canterbury, UK, April 4-7, 2004, Proceedings},
  booktitle = {IFM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2999},
  year      = {2004},
  isbn      = {3-540-21377-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Talks

• Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani:
  SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. 1-20
  
• Richard J. Boulton, Hanne Gottliebsen, Ruth Hardy, Tom Kelsey, Ursula Martin:
  Design Verification for Control Engineering. 21-35
  
• Thomas F. Melham:
  Integrating Model Checking and Theorem Proving in a Reflective Functional Language. 36-39
  

Tutorial

• Jim Woodcock, Ana Cavalcanti:
  A Tutorial Introduction to Designs in Unifying Theories of Programming. 40-66
  

Contributed Papers

• Bill J. Ellis, Andrew Ireland:
  An Integration of Program Analysis and Automated Theorem Proving. 67-86
  
• Steve Schneider, Helen Treharne:
  Verifying Controlled Components. 87-107
  
• Adalberto Farias, Alexandre Mota, Augusto Sampaio:
  Efficient CSP_Z Data Abstraction. 108-127
  
• Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha:
  State/Event-Based Software Model Checking. 128-147
  
• Kirsten Winter:
  Formalising Behaviour Trees with CSP. 148-167
  
• Jin Song Dong, Shengchao Qin, Jun Sun:
  Generating MSCs from an Integrated Formal Specification Language. 168-186
  
• Kevin Lano, David Clark, Kelly Androutsopoulos:
  UML to B: Formal Verification of Object-Oriented Models. 187-206
  
• Bernhard Beckert, Steffen Schlager:
  Software Verification with Integrated Data Type Refinement for Integer Arithmetic. 207-226
  
• Tiberiu Seceleanu, Juha Plosila:
  Constituent Elements of a Correctness-Preserving UML Design Approach. 227-246
  
• Xu Wang, A. W. Roscoe, Ranko Lazic:
  Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption. 247-266
  
• Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim:
  Linking CSP-OZ with UML and Java: A Case Study. 267-286
  
• Cécile Bui Thanh, Hanna Klaudel:
  Object-Oriented Modelling with High-Level Modular Petri Nets. 287-306
  
• Gabriel Ciobanu, Dorel Lucanu:
  Specification and Verification of Synchronizing Concurrent Objects. 307-327
  
• Steve Dunne:
  Understanding Object-Z Operations as Generalised Substitutions. 328-342
  
• Tim A. C. Willemse:
  Embeddings of Hybrid Automata in Process Algebra. 343-362
  
• Geguang Pu, Dang Van Hung, Jifeng He, Wang Yi:
  An Optimal Approach to Hardware/Software Partitioning for Synchronous Model. 363-381
  
• Ana Fernández Vilas, José J. Pazos Arias, Rebeca P. Díaz Redondo, Alberto Gil-Solla, Jorge García Duque:
  A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models. 382-401
  
• Yifeng Chen, Zhiming Liu:
  Integrating Temporal Logics. 402-420
  
• Marius C. Bujorianu:
  Integration of Specification Languages Using Viewpoints. 421-440
  
• Raymond T. Boute:
  Integrating Formal Methods by Unifying Abstractions. 441-460
  
• Paul Curzon, Ann Blandford:
  Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors. 461-480
  
• Simon Pickin, Jean-Marc Jézéquel:
  Using UML Sequence Diagrams as the Basis for a Formal Test Description Language. 481-500
  
• Luke Wildman, Roger Duke, Paul A. Strooper:
  Viewpoint-Based Testing of Concurrent Components. 501-520
  
• Francisco José Galán Morillo, José Miguel Cañete Valdeón:
  A Method for Compiling and Executing Expressive Assertions. 521-540