John S. Fitzgerald, Ian J. Hayes, Andrzej Tarlecki
Proceedings of the 13th International Symposium of Formal Methods Europe
FM, 2005.

@proceedings{FM-2005,
	address       = "Newcastle, United Kingdom",
	editor        = "John S. Fitzgerald and Ian J. Hayes and Andrzej Tarlecki",
	isbn          = "3-540-27882-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 13th International Symposium of Formal Methods Europe}",
	volume        = 3582,
	year          = 2005,
}

Contents (40 items)

8 ×#verification
7 ×#specification
5 ×#formal method
5 ×#model checking
5 ×#testing
3 ×#analysis
3 ×#modelling
3 ×#using
2 ×#approach
2 ×#automation

FM-2005-Joseph

Formal Aids for the Growth of Software Systems (MJ), p. 1.

FM-2005-Gaudel #approximate #correctness #formal method #testing

Formal Methods and Testing: Hypotheses, and Correctness Approximations (MCG), pp. 2–8.

FM-2005-Johnson #debugging #formal method #using

The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions (CWJ), pp. 9–25.

FM-2005-LeinoM #composition #invariant #verification

Modular Verification of Static Class Invariants (KRML, PM), pp. 26–42.

FM-2005-Kassios #object-oriented

Decoupling in Object Orientation (ITK), pp. 43–58.

FM-2005-PierikCB #using

Controlling Object Allocation Using Creation Guards (CP, DC, FSdB), pp. 59–74.

FM-2005-BouquetDLU #animation #ml #specification

Symbolic Animation of JML Specifications (FB, FD, BL, MU), pp. 75–90.

FM-2005-CacheraJPS #analysis #memory management

Certified Memory Usage Analysis (DC, TPJ, DP, GS), pp. 91–106.

FM-2005-CelikuM #composition #cost analysis #probability #source code #specification

Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs (OC, AM), pp. 107–122.

FM-2005-SalverdaRZ #parallel #verification

Formally Defining and Verifying Master/Slave Speculative Parallelization (PS, GR, CBZ), pp. 123–138.

FM-2005-WulfDR #implementation #modelling #realtime

Systematic Implementation of Real-Time Models (MDW, LD, JFR), pp. 139–156.

FM-2005-WassyngLH #safety

Timing Tolerances in Safety-Critical Software (AW, ML, XH), pp. 157–172.

FM-2005-BohnenkampB #testing

Timed Testing with TorX (HCB, AB), pp. 173–188.

FM-2005-RusuMJ #automation #consistency #safety #testing #validation #verification

Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems (VR, HM, TJ), pp. 189–204.

FM-2005-Bolton #csp

Adding Conflict and Confusion to CSP (CB), pp. 205–220.

FM-2005-ButlerL #csp #specification #verification

Combining CSP and B for Specification and Property Verification (MJB, ML), pp. 221–236.

FM-2005-WoodcockCF #model checking #semantics

Operational Semantics for Model Checking Circus (JW, AC, LF), pp. 237–252.

FM-2005-CavalcantiCO #diagrams

Control Law Diagrams in Circus (AC, PC, CO), pp. 253–268.

FM-2005-BasinKTW #architecture #verification

Verification of a Signature Architecture with HOL-Z (DAB, HK, KT, BW), pp. 269–285.

FM-2005-BuchholtzGHM #analysis #framework #performance #platform #security

End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform (MB, SG, VH, CM), pp. 286–301.

FM-2005-AndronickCP #embedded #security #smarttech #source code #verification

Formal Verification of Security Properties of Smart Card Embedded Source Code (JA, BC, CPM), pp. 302–317.

FM-2005-Zave #formal method #network

A Formal Model of Addressing for Interoperating Networks (PZ), pp. 318–333.

FM-2005-LeiI #approach #communication #protocol

An Approach to Unfolding Asynchronous Communication Protocols (YL, SPI), pp. 334–349.

FM-2005-QiuWPZ #fault #semantics

Semantics of BPEL4WS-Like Fault and Compensation Handling (ZQ, SW, GP, XZ), pp. 350–365.

FM-2005-Bosnacki #abstraction #calculus #on the #μ-calculus

On Some Galois Connection Based Abstractions for the μ-Calculus (DB), pp. 366–381.

FM-2005-BanachPJS #finite #sequence

Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern (RB, MP, CJ, SS), pp. 382–398.

FM-2005-AlvesSVO #sql #term rewriting

Strategic Term Rewriting and Its Application to a VDMSL to SQL Conversion (TLA, PFS, JV, JNO), pp. 399–414.

FM-2005-SunD #distributed #process #specification #synthesis

Synthesis of Distributed Processes from Scenario-Based Specifications (JS, JSD), pp. 415–431.

FM-2005-KatzK #specification #verification

Verifying Scenario-Based Aspect Specifications (EK, SK), pp. 432–447.

FM-2005-KimBC #approach #formal method #modelling #towards

An MDA Approach Towards Integrating Formal and Informal Modeling Languages (SKK, DB, DAC), pp. 448–464.

FM-2005-HoenickeM #model checking #process #specification

Model-Checking of Specifications Integrating Processes, Data and Time (JH, PM), pp. 465–480.

FM-2005-DonaldsonM #automation #detection #model checking #symmetry #using

Automatic Symmetry Detection for Model Checking Using Computational Group Theory (AFD, AM), pp. 481–496.

FM-2005-IyerSEJ #clustering #model checking #on the

On Partitioning and Symbolic Model Checking (SKI, DS, EAE, JJ), pp. 497–511.

FM-2005-SharyginaCCS #analysis #component

Dynamic Component Substitutability Analysis (NS, SC, EMC, NS), pp. 512–528.

FM-2005-Harrison #float #verification

Floating-Point Verification (JH), pp. 529–532.

FM-2005-EislerSJSS #case study #model checking

Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications (SE, CS, BJ, GS, JS), pp. 533–536.

FM-2005-Pretschner #modelling #testing

Model-Based Testing in Practice (AP), pp. 537–541.

FM-2005-CampbellGNSTV #concurrent #object-oriented #specification #testing

Testing Concurrent Object-Oriented Systems with Spec Explorer (CC, WG, LN, WS, NT, MV), pp. 542–547.

FM-2005-Broadfoot #cost analysis #formal method #industrial

ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software (GHB), pp. 548–551.

FM-2005-Muller

The Informal Nature of Systems Engineering (GM), pp. 552–556.