Michael J. Butler, Wolfram Schulte
Proceedings of the 17th International Symposium of Formal Methods
FM, 2011.

@proceedings{FM-2011,
	address       = "Limerick, Ireland",
	doi           = "10.1007/978-3-642-21437-0",
	editor        = "Michael J. Butler and Wolfram Schulte",
	isbn          = "978-3-642-21436-3",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 17th International Symposium of Formal Methods}",
	volume        = 6664,
	year          = 2011,
}

Contents (32 items)

12 ×#verification
5 ×#specification
3 ×#automation
2 ×#behaviour
2 ×#bound
2 ×#case study
2 ×#formal method
2 ×#memory management
2 ×#modelling
2 ×#relational

FM-2011-Sztipanovits #integration #perspective #physics #semantics

Model Integration and Cyber Physical Systems: A Semantics Perspective (JS), p. 1.

FM-2011-Harel #behaviour #programming

Some Thoughts on Behavioral Programming (DH), p. 2.

FM-2011-FisherPV

The Only Way Is Up (JF, NP, MYV), pp. 3–11.

FM-2011-DammF #question

Does It Pay to Extend the Perimeter of a World Model? (WD, BF), pp. 12–26.

FM-2011-DietschWP #verification

System Verification through Program Verification (DD, BW, AP), pp. 27–41.

FM-2011-LoosPN #adaptation #distributed #hybrid

Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified (SML, AP, LN), pp. 42–56.

FM-2011-BarringerH #analysis #domain-specific language #named #scala

TraceContract: A Scala DSL for Trace Analysis (HB, KH), pp. 57–72.

FM-2011-MullerR #using #verification

Using Debuggers to Understand Failed Verification Attempts (PM, JNR), pp. 73–87.

FM-2011-BonakdarpourNF #runtime #verification

Sampling-Based Runtime Verification (BB, SN, SF), pp. 88–102.

FM-2011-BoyerGS #configuration management #protocol #specification #verification

Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP (FB, OG, GS), pp. 103–117.

FM-2011-HaxthausenKB #automation #development #modelling #verification

Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems (AEH, AAK, MLB), pp. 118–132.

FM-2011-GhaziT #reasoning #relational #smt

Relational Reasoning via SMT Solving (AAEG, MT), pp. 133–148.

FM-2011-AmalioGK #automation #generative #modelling #specification

Building VCL Models and Automatically Generating Z Specifications from Them (NA, CG, PK), pp. 149–153.

FM-2011-KlebanovMSLWAABCCHJLMPPRSTTUW #case study #contest #experience

The 1st Verified Software Competition: Experience Report (VK, PM, NS, GTL, VW, EA, RA, DB, RC, EC, MAH, BJ, KRML, RM, FP, NP, TR, JS, ST, TT, MU, BW), pp. 154–168.

FM-2011-Li #compilation #logic

Validated Compilation through Logic (GL), pp. 169–183.

FM-2011-DiosP #bound #certification #memory management #polynomial

Certification of Safe Polynomial Memory Bounds (JdD, RP), pp. 184–199.

FM-2011-BartheCK #relational #source code #using #verification

Relational Verification Using Product Programs (GB, JMC, CK), pp. 200–214.

FM-2011-BanksJ #specification

Specifying Confidentiality in Circus (MJB, JLJ), pp. 215–230.

FM-2011-BartheBCL #verification

Formally Verifying Isolation and Availability in an Idealized Model of Virtualization (GB, GB, JDC, CL), pp. 231–245.

FM-2011-CavalcantiWW #formal method #java #memory management #safety

The Safety-Critical Java Memory Model: A Formal Account (AC, AJW, JW), pp. 246–261.

FM-2011-ChenLW #communication #process #refinement

Failure-Divergence Refinement of Compensating Communicating Processes (ZC, ZL, JW), pp. 262–277.

FM-2011-Dunne #csp #termination

Termination without √ in CSP (SD), pp. 278–292.

FM-2011-CiobanuK #interactive #migration

Timed Migration and Interaction with Access Permissions (GC, MK), pp. 293–307.

FM-2011-BowenR #case study #community #formal method

From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community (JPB, SR), pp. 308–322.

FM-2011-DerrickSW #verification

Verifying Linearisability with Potential Linearisation Points (JD, GS, HW), pp. 323–337.

FM-2011-MeryMT #algorithm #verification

Refinement-Based Verification of Local Synchronization Algorithms (DM, MM, MT), pp. 338–352.

FM-2011-AlbertGGJST #behaviour #bound #concurrent #simulation #worst-case

Simulating Concurrent Behaviors with Worst-Case Cost Bounds (EA, SG, MGZ, EBJ, RS, SLTT), pp. 353–368.

FM-2011-QinLCH #automation #specification #verification

Automatically Refining Partial Specifications for Program Verification (SQ, CL, WNC, GH), pp. 369–385.

FM-2011-GherghinaDQC #source code #specification #verification

Structured Specifications for Better Verification of Heap-Manipulating Programs (CG, CD, SQ, WNC), pp. 386–401.

FM-2011-JacobsSP #verification

Verification of Unloadable Modules (BJ, JS, FP), pp. 402–416.

FM-2011-RozierV #approach #encoding #ltl #multi #satisfiability

A Multi-encoding Approach for LTL Symbolic Satisfiability Checking (KYR, MYV), pp. 417–431.

FM-2011-ZhangSPLD #on the #reduction

On Combining State Space Reductions with Global Fairness Assumptions (SJZ, JS, JP, YL, JSD), pp. 432–447.