Elvira Albert, Emil Sekerinski
Proceedings of the 11th International Conference on Integrated Formal Methods
IFM, 2014.

@proceedings{IFM-2014,
	address       = "Bertinoro, Italy",
	doi           = "10.1007/978-3-319-10181-1",
	editor        = "Elvira Albert and Emil Sekerinski",
	isbn          = "978-3-319-10180-4",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 11th International Conference on Integrated Formal Methods}",
	volume        = 8739,
	year          = 2014,
}

Contents (23 items)

5 ×#verification
4 ×#analysis
3 ×#modelling
3 ×#proving
3 ×#security
2 ×#protocol
2 ×#refinement
2 ×#semantics
2 ×#specification
2 ×#theorem proving

IFM-2014-CalvaneseKSVZ #analysis #data type

Shape and Content — A Database-Theoretic Perspective on the Analysis of Data Structures (DC, TK, MS, HV, FZ), pp. 3–17.

IFM-2014-DrossopoulouN #how #policy #semantics

How to Break the Bank: Semantics of Capability Policies (SD, JN), pp. 18–35.

IFM-2014-OliveiraSF #model checking #specification

Model-Checking Circus State-Rich Specifications (MVMO, ACAS, MSCF), pp. 39–54.

IFM-2014-HentschelKHB #ide #interactive #verification

An Interactive Verification Tool Meets an IDE (MH, SK, RH, RB), pp. 55–70.

IFM-2014-GilmoreTV #analysis #evaluation

An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems (SG, MT, AV), pp. 71–86.

IFM-2014-AbbasBR #modelling #uml

Modeling UML Template Classes with FoCaLiZe (MA, CBBY, RR), pp. 87–102.

IFM-2014-LaibinisBPTTP #in the cloud #modelling #simulation

Integrating Event-B Modelling and Discrete-Event Simulation to Analyse Resilience of Data Stores in the Cloud (LL, BB, IP, ET, KET, IP), pp. 103–119.

IFM-2014-FathabadiSB #manycore #modelling #process #runtime

Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems (ASF, CFS, MJB), pp. 120–135.

IFM-2014-MellerGY #behaviour #uml #verification

Verifying Behavioral UML Systems via CEGAR (YM, OG, KY), pp. 139–154.

IFM-2014-MiyazawaC #refinement

Formal Refinement in SysML (AM, AC), pp. 155–170.

IFM-2014-BrideKP #constraints #specification #theorem proving #using #verification #workflow

Verifying Modal Workflow Specifications Using Constraint Solving (HB, OK, FP), pp. 171–186.

IFM-2014-ErikssonPB #invariant #programming #proving

Proofs and Refutations in Invariant-Based Programming (JE, MP, RJB), pp. 189–204.

IFM-2014-ChaudhariD #automation #proving #theorem proving

Automated Theorem Prover Assisted Program Calculations (DLC, OPD), pp. 205–220.

IFM-2014-SchneiderTWW #ltl #refinement

Managing LTL Properties in Event-B Refinement (SAS, HT, HW, DMW), pp. 221–237.

IFM-2014-BruniSNN #analysis #protocol #security

Formal Security Analysis of the MaCAN Protocol (AB, MS, FN, HRN), pp. 241–255.

IFM-2014-KordyPS #framework #probability #security

A Probabilistic Framework for Security Scenarios with Dependent Actions (BK, MP, PS), pp. 256–271.

IFM-2014-RamsdellDGR #analysis #hybrid #protocol #security

A Hybrid Analysis for Security Protocols with State (JDR, DJD, JDG, PDR), pp. 272–287.

IFM-2014-AsavoaeAR #interprocedural #semantics #slicing #towards

Towards a Formal Semantics-Based Technique for Interprocedural Slicing (IMA, MA, AR), pp. 291–306.

IFM-2014-JakobsPWW #hardware #verification

Integrating Software and Hardware Verification (MCJ, MP, HW, TW), pp. 307–322.

IFM-2014-FurstHBDSM #code generation

Code Generation for Event-B (AF, TSH, DAB, KD, NS, KM), pp. 323–338.

IFM-2014-DerrickSD #architecture #verification

Verifying Linearizability on TSO Architectures (JD, GS, BD), pp. 341–356.

IFM-2014-TofanSR #composition #multi #proving

A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset (BT, GS, WR), pp. 357–372.

IFM-2014-PatcasLM #embedded

A Separation Principle for Embedded System Interfacing (LMP, ML, TSEM), pp. 373–388.