Eerke A. Boiten, John Derrick, Graeme Smith
Proceedings of the Fourth International Conference on Integrated Formal Methods
IFM, 2004.

@proceedings{IFM-2004,
	address       = "Canterbury, England, United Kingdom",
	editor        = "Eerke A. Boiten and John Derrick and Graeme Smith",
	isbn          = "3-540-21377-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Conference on Integrated Formal Methods}",
	volume        = 2999,
	year          = 2004,
}

Contents (28 items)

6 ×#verification
4 ×#design
4 ×#specification
4 ×#uml
3 ×#formal method
3 ×#modelling
2 ×#abstraction
2 ×#approach
2 ×#case study
2 ×#component

IFM-2004-BallCLR #formal method #verification

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (TB, BC, VL, SKR), pp. 1–20.

IFM-2004-BoultonGHKM #design #verification

Design Verification for Control Engineering (RJB, HG, RH, TK, UM), pp. 21–35.

IFM-2004-Melham #functional #model checking #proving #theorem proving

Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.

IFM-2004-WoodcockC #design #programming #tutorial

A Tutorial Introduction to Designs in Unifying Theories of Programming (JW, AC), pp. 40–66.

IFM-2004-EllisI #automation #integration #program analysis #proving #theorem proving

An Integration of Program Analysis and Automated Theorem Proving (BJE, AI), pp. 67–86.

IFM-2004-SchneiderT #component #verification

Verifying Controlled Components (SS, HT), pp. 87–107.

IFM-2004-FariasMS #abstraction #performance

Efficient CSPZ Data Abstraction (AF, AM, AS), pp. 108–127.

IFM-2004-ChakiCOSS #model checking

State/Event-Based Software Model Checking (SC, EMC, JO, NS, NS), pp. 128–147.

IFM-2004-Winter #behaviour #csp #formal method

Formalising Behaviour Trees with CSP (KW), pp. 148–167.

IFM-2004-DongQS #generative #specification

Generating MSCs from an Integrated Formal Specification Language (JSD, SQ, JS), pp. 168–186.

IFM-2004-LanoCA #modelling #object-oriented #uml #verification

UML to B: Formal Verification of Object-Oriented Models (KL, DC, KA), pp. 187–206.

IFM-2004-BeckertS #data type #integer #refinement #verification

Software Verification with Integrated Data Type Refinement for Integer Arithmetic (BB, SS), pp. 207–226.

IFM-2004-SeceleanuP #approach #design #uml

Constituent Elements of a Correctness-Preserving UML Design Approach (TS, JP), pp. 227–246.

IFM-2004-WangRL #csp #independence #reachability

Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption (XW, AWR, RL), pp. 247–266.

IFM-2004-MollerORW #case study #java #uml

Linking CSP-OZ with UML and Java: A Case Study (MM, ERO, HR, HW), pp. 267–286.

IFM-2004-ThanhK #composition #modelling #object-oriented #petri net

Object-Oriented Modelling with High-Level Modular Petri Nets (CBT, HK), pp. 287–306.

IFM-2004-CiobanuL #concurrent #specification #verification

Specification and Verification of Synchronizing Concurrent Objects (GC, DL), pp. 307–327.

IFM-2004-Dunne #comprehension

Understanding Object-Z Operations as Generalised Substitutions (SD), pp. 328–342.

IFM-2004-Willemse #algebra #automaton #hybrid #process

Embeddings of Hybrid Automata in Process Algebra (TACW), pp. 343–362.

IFM-2004-PuHHY #approach #clustering #hardware

An Optimal Approach to Hardware/Software Partitioning for Synchronous Model (GP, DVH, JH, WY), pp. 363–381.

IFM-2004-VilasARGD #imperative #incremental #logic #modelling #semantics #specification

A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models (AFV, JJPA, RPDR, AGS, JGD), pp. 382–401.

IFM-2004-ChenL #logic

Integrating Temporal Logics (YC, ZL), pp. 402–420.

IFM-2004-Bujorianu #integration #specification #using

Integration of Specification Languages Using Viewpoints (MCB), pp. 421–440.

IFM-2004-Boute #abstraction #formal method

Integrating Formal Methods by Unifying Abstractions (RTB), pp. 441–460.

IFM-2004-CurzonB #case study #design #fault

Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors (PC, AB), pp. 461–480.

IFM-2004-PickinJ #diagrams #sequence chart #uml #using

Using UML Sequence Diagrams as the Basis for a Formal Test Description Language (SP, JMJ), pp. 481–500.

IFM-2004-WildmanDS #component #concurrent #testing

Viewpoint-Based Testing of Concurrent Components (LW, RD, PAS), pp. 501–520.

IFM-2004-MorilloV #compilation

A Method for Compiling and Executing Expressive Assertions (FJGM, JMCV), pp. 521–540.