John Derrick, Stefania Gnesi, Diego Latella, Helen Treharne
Proceedings of the Ninth International Conference on Integrated Formal Methods
IFM, 2012.

@proceedings{IFM-2012,
	address       = "Pisa, Italy",
	doi           = "10.1007/978-3-642-30729-4",
	editor        = "John Derrick and Stefania Gnesi and Diego Latella and Helen Treharne",
	isbn          = "978-3-642-30728-7",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Ninth International Conference on Integrated Formal Methods}",
	volume        = 7321,
	year          = 2012,
}

Contents (24 items)

5 ×#verification
4 ×#modelling
3 ×#network
3 ×#source code
2 ×#analysis
2 ×#detection
2 ×#framework
2 ×#generative
2 ×#interactive
2 ×#java

IFM-2012-BorgerCG #analysis #framework #web

Contribution to a Rigorous Analysis of Web Application Frameworks (EB, AC, VG), pp. 1–20.

IFM-2012-CalderS #algebra #case study #network #process #runtime #verification

Process Algebra for Event-Driven Runtime Verification: A Case Study of Wireless Network Management (MC, MS), pp. 21–23.

IFM-2012-HansenL #validation

Translating TLA + to B for Validation with ProB (DH, ML), pp. 24–38.

IFM-2012-DongolH #multi #reasoning #source code

Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands (BD, IJH), pp. 39–53.

IFM-2012-IsobeMNR #approach #capacity #csp #safety

Safety and Line Capacity in Railways — An Approach in Timed CSP (YI, FM, HNN, MR), pp. 54–68.

IFM-2012-BerthingBSTV #development

Refinement-Based Development of Timed Systems (JB, PB, KS, LT, JV), pp. 69–83.

IFM-2012-BlackmoreHBER #automation #generative #simulation #verification

Analysing and Closing Simulation Coverage by Automatic Generation and Verification of Formal Properties from Coverage Reports (TB, DH, PB, KE, NR), pp. 84–98.

IFM-2012-ZhangNN #model checking #revisited #static analysis

Model Checking as Static Analysis: Revisited (FZ, FN, HRN), pp. 99–112.

IFM-2012-NgoTGGB #compilation #equation #verification

Formal Verification of Compiler Transformations on Polychronous Equations (VCN, JPT, TG, PLG, LB), pp. 113–127.

IFM-2012-RochaBCN #bound #comprehension #debugging #model checking #programming #using

Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples (HR, RSB, LCC, ADN), pp. 128–142.

IFM-2012-KazemeyniJOB #analysis #modelling #network #probability

MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis (FK, EBJ, OO, IB), pp. 143–157.

IFM-2012-WoehrleBM #anti #network

Mechanized Extraction of Topology Anti-patterns in Wireless Networks (MW, RB, MRM), pp. 158–173.

IFM-2012-LensinkSE #concurrent #framework #proving #source code

A Proof Framework for Concurrent Programs (LL, SS, MCJDvE), pp. 174–190.

IFM-2012-BrescianiB #semantics

A UTP Semantics of pGCL as a Homogeneous Relation (RB, AB), pp. 191–205.

IFM-2012-TianBB #behaviour #detection #game studies #multi

Behaviour-Based Cheat Detection in Multiplayer Games with Event-B (HT, PJB, AGB), pp. 206–220.

IFM-2012-DiaconescuLPSS #interactive

Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems (DD, IL, LP, KS, GS), pp. 221–236.

IFM-2012-TarasyukTL #formal method #modelling #probability #verification

Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B (AT, ET, LL), pp. 237–252.

IFM-2012-MarkovskiBB #component #requirements

Partially-Supervised Plants: Embedding Control Requirements in Plant Components (JM, DAvB, JCMB), pp. 253–267.

IFM-2012-HoomanMW #abstraction #detection #fault #industrial #modelling #using

Early Fault Detection in Industry Using Models at Various Abstraction Levels (JH, AJM, HvW), pp. 268–282.

IFM-2012-JiB #java #named #source code

PE-KeY: A Partial Evaluator for Java Programs (RJ, RB), pp. 283–295.

IFM-2012-AndradeFLP #generative #java #testing

Specification-Driven Unit Test Generation for Java Generic Classes (FRdA, JPF, AL, ACRP), pp. 296–311.

IFM-2012-GarisPCR #alloy #protocol #specification #state machine #uml

Specifying UML Protocol State Machines in Alloy (AGG, ACRP, AC, DR), pp. 312–326.

IFM-2012-SchunselaarMS #declarative #modelling

Patterns for a Log-Based Strengthening of Declarative Compliance Models (DMMS, FMM, NS), pp. 327–342.

IFM-2012-RochaCMS #execution #interactive #verification

A Formal Interactive Verification Environment for the Plan Execution Interchange Language (CR, HC, CAM, RS), pp. 343–357.