Einar Broch Johnsen, Luigia Petre
Proceedings of the 10th International Conference on Integrated Formal Methods
IFM, 2013.

@proceedings{IFM-2013,
	address       = "Turku, Finland",
	doi           = "10.1007/978-3-642-38613-8",
	editor        = "Einar Broch Johnsen and Luigia Petre",
	isbn          = "['978-3-642-38612-1', '978-3-642-38613-8']",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 10th International Conference on Integrated Formal Methods}",
	volume        = 7940,
	year          = 2013,
}

Contents (29 items)

7 ×#verification
3 ×#automation
3 ×#behaviour
3 ×#distributed
3 ×#modelling
3 ×#semantics
3 ×#using
2 ×#algorithm
2 ×#analysis
2 ×#automaton

IFM-2013-Abrial #proving #source code

From Z to B and then Event-B: Assigning Proofs to Meaningful Programs (JRA), pp. 1–15.

IFM-2013-HudonH #design

Systems Design Guided by Progress Concerns (SH, TSH), pp. 16–30.

IFM-2013-Prehofer #behaviour #diagrams #refinement #specification

Assume-Guarantee Specifications of State Transition Diagrams for Behavioral Refinement (CP), pp. 31–45.

IFM-2013-Lausdahl #alloy

Translating VDM to Alloy (KL), pp. 46–60.

IFM-2013-VekrisLDM #specification #using #verification

Verification of EB3 Specifications Using CADP (DV, FL, CD, RM), pp. 61–76.

IFM-2013-GrafQ #distributed #implementation

Knowledge for the Distributed Implementation of Constrained Systems (SG, SQ), pp. 77–93.

IFM-2013-MoranHS #automation #verification

Automated Anonymity Verification of the ThreeBallot Voting System (MM, JH, SS), pp. 94–108.

IFM-2013-MilloRKN #composition #product line #verification

Compositional Verification of Software Product Lines (JVM, SR, SNK, GKN), pp. 109–123.

IFM-2013-GavaFG #algorithm #deduction #verification

Deductive Verification of State-Space Algorithms (FG, JF, MG), pp. 124–138.

IFM-2013-IshiiMN #automaton #calculus #hybrid #induction #verification

Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus (DI, GM, SN), pp. 139–153.

IFM-2013-Larsen #automaton #model checking #statistics

Priced Timed Automata and Statistical Model Checking (KGL), pp. 154–161.

IFM-2013-Song00LD #analysis #divide and conquer #reachability

Improved Reachability Analysis in DTMC via Divide and Conquer (SS, LG, JS, YL, JSD), pp. 162–176.

IFM-2013-MorgensternGS #game studies #incremental #induction #using

Solving Games Using Incremental Induction (AM, MG, KS), pp. 177–191.

IFM-2013-SongT #api #library #model checking

Model-Checking Software Library API Usage Rules (FS, TT), pp. 192–207.

IFM-2013-MeryP #formal method #modelling #protocol #verification

Formal Modelling and Verification of Population Protocols (DM, MP), pp. 208–222.

IFM-2013-SavaryFL #bytecode #detection #modelling #testing #using #verification

Detecting Vulnerabilities in Java-Card Bytecode Verifiers Using Model-Based Testing (AS, MF, JLL), pp. 223–237.

IFM-2013-RuksenasCH #behaviour #evaluation #interactive #predict

Integrating Formal Predictions of Interactive System Behaviour with User Evaluation (RR, PC, MDH), pp. 238–252.

IFM-2013-TaylorBD #automation #behaviour #erlang

Automatic Inference of Erlang Module Behaviour (RT, KB, JD), pp. 253–267.

IFM-2013-AndriamiarinaMS #algorithm #distributed #modelling

Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms (MBA, DM, NKS), pp. 268–284.

IFM-2013-AlbertCPR #abstraction #distributed #quantifier

Quantified Abstractions of Distributed Systems (EA, JC, GP, GRD), pp. 285–300.

IFM-2013-LaneveP #algebra #contract #web #web service

An Algebraic Theory for Web Service Contracts (CL, LP), pp. 301–315.

IFM-2013-CastillosDJKT #composition #semantics

A Compositional Automata-Based Semantics for Property Patterns (KCC, FD, JJ, BK, ST), pp. 316–330.

IFM-2013-LiuLACSWD #semantics #state machine #uml

A Formal Semantics for Complete UML State Machines with Communications (SL, YL, ÉA, CC, JS, BW, JSD), pp. 331–346.

IFM-2013-Ciobaca #automation #semantics

From Small-Step Semantics to Big-Step Semantics, Automatically (SC), pp. 347–361.

IFM-2013-LucanuR #equivalence #reasoning

Program Equivalence by Circular Reasoning (DL, VR), pp. 362–377.

IFM-2013-OlderogS #realtime

Structural Transformations for Data-Enriched Real-Time Systems (ERO, MS), pp. 378–393.

IFM-2013-GiachinoGLLW #analysis #concurrent #theory and practice

Deadlock Analysis of Concurrent Objects: Theory and Practice (EG, CAG, CL, ML, PYHW), pp. 394–411.

IFM-2013-VigoNN #communication

Broadcast, Denial-of-Service, and Secure Communication (RV, FN, HRN), pp. 412–427.

IFM-2013-DemasiCMA #fault tolerance #simulation

Characterizing Fault-Tolerant Systems by Means of Simulation Relations (RD, PFC, TSEM, NA), pp. 428–442.