Proceedings of the 17th International Symposium of Formal Methods
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

FM
DBLP
Scholar
DOI
Full names Links ISxN
@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)

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.