Jorge Cuéllar, Thomas Stephen Edward Maibaum, Kaisa Sere
Proceedings of the 15th International Symposium of Formal Methods
FM, 2008.

@proceedings{FM-2008,
	address       = "Turku, Finland",
	editor        = "Jorge Cuéllar and Thomas Stephen Edward Maibaum and Kaisa Sere",
	isbn          = "978-3-540-68235-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 15th International Symposium of Formal Methods}",
	volume        = 5014,
	year          = 2008,
}

Contents (32 items)

6 ×#formal method
6 ×#specification
5 ×#verification
4 ×#development
3 ×#case study
3 ×#security
2 ×#analysis
2 ×#declarative
2 ×#distributed
2 ×#experience

FM-2008-Katz #aspect-oriented #formal method

Aspects and Formal Methods (SK), pp. 1–11.

FM-2008-ArvindDK #design #verification

Getting Formal Verification into Design Flow (A, ND, MK), pp. 12–32.

FM-2008-Engler #case study #experience #lessons learnt #scalability

Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems (DRE), p. 33.

FM-2008-KitchinPM #distributed #logic #simulation

Simulation, Orchestration and Logical Clocks (DK, EP, JM), p. 34.

FM-2008-ZaksP #compilation #named #program analysis #validation

CoVaC: Compiler Validation by Program Analysis of the Cross-Product (AZ, AP), pp. 35–51.

FM-2008-DovlandJOS #behaviour #lazy evaluation #type system

Lazy Behavioral Subtyping (JD, EBJ, OO, MS), pp. 52–67.

FM-2008-RudichDM #specification

Checking Well-Formedness of Pure-Method Specifications (AR, ÁD, PM), pp. 68–83.

FM-2008-NollR #pointer #thread #verification

Verifying Dynamic Pointer-Manipulating Threads (TN, SR), pp. 84–99.

FM-2008-McIverMG #probability #proving #refinement

Proofs and Refutations for Probabilistic Refinement (AKM, CCM, CG), pp. 100–115.

FM-2008-EmmiGP #automaton #interface #verification

Assume-Guarantee Verification for Interface Automata (ME, DG, CSP), pp. 116–131.

FM-2008-FuriaPR #approximate #automation #specification #verification

Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation (CAF, MP, MR), pp. 132–147.

FM-2008-MateescuT #concurrent #model checking

A Model Checking Language for Concurrent Value-Passing Systems (RM, DT), pp. 148–164.

FM-2008-GrandyBSSR #protocol #security #verification

Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code (HG, MB, KS, GS, WR), pp. 165–180.

FM-2008-MacedoLF #development #distributed #incremental #realtime #using

Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM (HDM, PGL, JSF), pp. 181–197.

FM-2008-ChetaliN #evaluation #formal method #industrial #security #using

Industrial Use of Formal Methods for a High-Level Security Evaluation (BC, QHN), pp. 198–213.

FM-2008-KiniryZ #formal method

Secret Ninja Formal Methods (JRK, DMZ), pp. 214–228.

FM-2008-AmtoftHRRHG #contract #data flow #specification

Specification and Checking of Software Contracts for Conditional Information Flow (TA, JH, ER, R, JH, DG), pp. 229–245.

FM-2008-ChalinR #fault #ml #performance #runtime #using

JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity (PC, FR), pp. 246–261.

FM-2008-AktugDG #monitoring #runtime

Provably Correct Runtime Monitoring (IA, MD, DG), pp. 262–277.

FM-2008-PonsiniS #modelling #semantics

A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOS (OP, WS), pp. 278–293.

FM-2008-RidgeNS #approach #implementation #network #protocol

A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service (TR, MN, PS), pp. 294–309.

FM-2008-UzuncaovaK #analysis #constraints #declarative #modelling #performance

Constraint Prioritization for Efficient Analysis of Declarative Models (EU, SK), pp. 310–325.

FM-2008-TorlakCJ #declarative #satisfiability #specification

Finding Minimal Unsatisfiable Cores of Declarative Specifications (ET, FSHC, DJ), pp. 326–341.

FM-2008-GawlitzaS #analysis #game studies #precise

Precise Interval Analysis vs. Parity Games (TG, HS), pp. 342–357.

FM-2008-McCombS #refinement

Introducing Objects through Refinement (TM, GS), pp. 358–373.

FM-2008-BonakdarpourK #bound #fault

Masking Faults While Providing Bounded-Time Phased Recovery (BB, SSK), pp. 374–389.

FM-2008-HarhurinH #consistency #product line #specification #towards

Towards Consistent Specifications of Product Families (AH, JH), pp. 390–405.

FM-2008-LintelmanRLS #formal method #security

Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets Distribution (SL, RR, ML, KS), pp. 406–410.

FM-2008-VerhulstJM #case study #development #formal method #industrial

An Industrial Case: Pitfalls and Benefits of Applying Formal Methods to the Development of a Network-Centric RTOS (EV, GGdJ, VM), pp. 411–418.

FM-2008-WijbransBRG #case study #development #experience #formal method #re-engineering

Software Engineering with Formal Methods: Experiences with the Development of a Storm Surge Barrier Control System (KW, FB, RR, WG), pp. 419–424.

FM-2008-KuritaCN #development #mobile #specification

Application of a Formal Specification Language in the Development of the “Mobile FeliCa” IC Chip Firmware for Embedding in Mobile Phone (TK, MC, YN), pp. 425–429.

FM-2008-Lecomte #framework #platform #reliability

Safe and Reliable Metro Platform Screen Doors Control/Command Systems (TL), pp. 430–434.