Ana Cavalcanti, Dennis Dams
Proceedings of the 16th International Symposium of Formal Methods: Second World Congress
FM, 2009.

@proceedings{FM-2009,
	address       = "Eindhoven, The Netherlands",
	doi           = "10.1007/978-3-642-05089-3",
	editor        = "Ana Cavalcanti and Dennis Dams",
	isbn          = "978-3-642-05088-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 16th International Symposium of Formal Methods: Second World Congress}",
	volume        = 5850,
	year          = 2009,
}

Contents (53 items)

10 ×#verification
5 ×#analysis
5 ×#bound
5 ×#formal method
5 ×#refinement
5 ×#using
4 ×#abstraction
4 ×#composition
4 ×#model checking
4 ×#semantics

FM-2009-TschantzW #formal method #privacy

Formal Methods for Privacy (MCT, JMW), pp. 1–15.

FM-2009-BonzanniFFK #biology #formal method #question #what

What Can Formal Methods Bring to Systems Biology? (NB, KAF, WF, EK), pp. 16–22.

FM-2009-OHalloran #verification

Guess and Verify — Back to the Future (CO), pp. 23–32.

FM-2009-Rajamani #statistics #testing #verification

Verification, Testing and Statistics (SKR), pp. 33–40.

FM-2009-McIverMM #probability #security

Security, Probability and Nearly Fair Coins in the Cryptographers’ Café (AM, LM, CM), pp. 41–71.

FM-2009-JaffarS #abstraction #recursion

Recursive Abstractions for Parameterized Systems (JJ, AES), pp. 72–88.

FM-2009-Tonetta #abstraction #model checking

Abstract Model Checking without Computing the Abstraction (ST), pp. 89–105.

FM-2009-SchriebWW #abstraction

Three-Valued Spotlight Abstractions (JS, HW, DW), pp. 106–122.

FM-2009-SunLRLD #abstraction #model checking #process

Fair Model Checking with Process Counter Abstraction (JS, YL, AR, SL, JSD), pp. 123–139.

FM-2009-RamosSM #component #development

Systematic Development of Trustworthy Component Systems (RR, AS, AM), pp. 140–156.

FM-2009-LangM #composition #confluence #detection #partial order #reduction #using

Partial Order Reductions Using Compositional Confluence Detection (FL, RM), pp. 157–172.

FM-2009-JeffordsHAL #composition #fault tolerance #formal method #refinement #using

A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition (RDJ, CLH, MA, EIL), pp. 173–189.

FM-2009-SchierlSHR #file system #memory management #specification

Abstract Specification of the UBIFS File System for Flash Memory (AS, GS, DH, WR), pp. 190–206.

FM-2009-ShahbazG #automaton

Inferring Mealy Machines (MS, RG), pp. 207–222.

FM-2009-KohlhaseLSS #process

Formal Management of CAD/CAM Processes (MK, JL, LS, ES), pp. 223–238.

FM-2009-Eshuis #petri net

Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way (RE), pp. 239–255.

FM-2009-WangKGG #analysis #concurrent #predict #source code

Symbolic Predictive Analysis for Concurrent Programs (CW, SK, MKG, AG), pp. 256–272.

FM-2009-DaylightS #case study #design #on the

On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study (EGD, SKS), pp. 273–288.

FM-2009-McIverM #case study #composition #refinement #security

Sums and Lovers: Case Studies in Security, Compositionality and Refinement (AM, CCM), pp. 289–304.

FM-2009-WalkinshawDG #modelling #refinement #testing

Iterative Refinement of Reverse-Engineered Models by Model-Based Testing (NW, JD, QG), pp. 305–320.

FM-2009-LiuCLS #model checking #refinement

Model Checking Linearizability via Refinement (YL, WC, YAL, JS), pp. 321–337.

FM-2009-HoenickeLPSW

It’s Doomed; We Can Prove It (JH, KRML, AP, MS, TW), pp. 338–353.

FM-2009-JostLHSH #analysis #bound #using

“Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis (SJ, HWL, KH, NS, MH), pp. 354–369.

FM-2009-AlbertAGP #analysis

Field-Sensitive Value Analysis by Field-Insensitive Analysis (EA, PA, SG, GP), pp. 370–386.

FM-2009-Boute #logic #unification

Making Temporal Logic Calculational: A Tool for Unification and Discovery (RTB), pp. 387–402.

FM-2009-Reynolds

A Tableau for CTL (MR), pp. 403–418.

FM-2009-LuthW #c #source code #specification #verification

Certifiable Specification and Verification of C Programs (CL, DW), pp. 419–434.

FM-2009-HasanAATA #random #reasoning

Formal Reasoning about Expectation Properties for Continuous Random Variables (OH, NA, BA, ST, RA), pp. 435–450.

FM-2009-GancarskiB #semantics

The Denotational Semantics of slotted-Circus (PG, AB), pp. 451–466.

FM-2009-ChenS #nondeterminism #probability

Unifying Probability with Nondeterminism (YC, JWS), pp. 467–482.

FM-2009-GiannakopoulosDFK #alloy #semantics #towards

Towards an Operational Semantics for Alloy (TG, DJD, KF, SK), pp. 483–498.

FM-2009-ReevesS #fault #robust #semantics

A Robust Semantics Hides Fewer Errors (SR, DS), pp. 499–515.

FM-2009-HeidarianSV #analysis #network #protocol

Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks (FH, JS, FWV), pp. 516–531.

FM-2009-SouyrisWDD #verification

Formal Verification of Avionics Software Products (JS, VW, DD, HD), pp. 532–546.

FM-2009-PlatzerC #case study #verification

Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study (AP, EMC), pp. 547–562.

FM-2009-LausdahlLL #tool support #uml

Connecting UML and VDM++ with Open Tool Support (KL, HKAL, PGL), pp. 563–578.

FM-2009-SaidBS #refinement #state machine #tool support #uml

Language and Tool Support for Class and State Machine Refinement in UML-B (MYS, MJB, CFS), pp. 579–595.

FM-2009-JohnsenKY #composition #concurrent #distributed #evolution

Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects (EBJ, MK, ICY), pp. 596–611.

FM-2009-AhrendtBG #logic

Abstract Object Creation in Dynamic Logic (WA, FSdB, IG), pp. 612–627.

FM-2009-Gast #memory management #reasoning

Reasoning about Memory Layouts (HG), pp. 628–643.

FM-2009-SeidlVV #alias #analysis #linear #polynomial

A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis (HS, VV, VV), pp. 644–659.

FM-2009-BonakdarpourK #bound #complexity #on the

On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery (BB, SSK), pp. 660–675.

FM-2009-LarsenLNP #realtime #requirements #verification

Verifying Real-Time Systems against Scenario-Based Requirements (KGL, SL, BN, SP), pp. 676–691.

FM-2009-GomesO #specification

Formal Specification of a Cardiac Pacing System (AOG, MVMO), pp. 692–707.

FM-2009-LeuschelFFP #automation #modelling #scalability #verification

Automated Property Verification for Large Scale B Models (ML, JF, FF, DP), pp. 708–723.

FM-2009-VakkalankaVGK #execution #semantics #theory and practice

Reduced Execution Semantics of MPI: From Theory to Practice (SSV, AV, GG, RMK), pp. 724–740.

FM-2009-PradellaMP #bound #encoding #metric #model checking

A Metric Encoding for Bounded Model Checking (MP, AM, PSP), pp. 741–756.

FM-2009-ShaoKP #approach #bound #formal method #incremental #lightweight #using

An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method (DS, SK, DEP), pp. 757–772.

FM-2009-HarrisKCJR #bound #data flow #process #verification

Verifying Information Flow Control over Unbounded Processes (WRH, NK, SC, SJ, TWR), pp. 773–789.

FM-2009-AlpuenteBR #logic #specification #verification #web

Specification and Verification of Web Applications in Rewriting Logic (MA, DB, DR), pp. 790–805.

FM-2009-LeinenbachS #verification

Verifying the Microsoft Hyper-V Hypervisor with VCC (DL, TS), pp. 806–809.

FM-2009-BicarreguiFLW #formal method #industrial #overview #perspective

Industrial Practice in Formal Methods: A Review (JB, JSF, PGL, JCPW), pp. 810–813.

FM-2009-HjortRLPS #modelling #testing #user interface #using

Model-Based GUI Testing Using Uppaal at Novo Nordisk (UHH, JIR, KGL, MAP, AS), pp. 814–818.