Gilles Barthe, Alberto Pardo, Gerardo Schneider
Proceedings of the Ninth International Conference on Software Engineering and Formal Methods
SEFM, 2011.

@proceedings{SEFM-2011,
	address       = "Montevideo, Uruguay",
	doi           = "10.1007/978-3-642-24690-6",
	editor        = "Gilles Barthe and Alberto Pardo and Gerardo Schneider",
	isbn          = "978-3-642-24689-0",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Ninth International Conference on Software Engineering and Formal Methods}",
	volume        = 7041,
	year          = 2011,
}

Contents (34 items)

10 ×#verification
5 ×#analysis
5 ×#formal method
4 ×#specification
3 ×#hybrid
3 ×#logic
3 ×#modelling
3 ×#process
3 ×#using
2 ×#approach

SEFM-2011-Hermanns #energy #formal method

Formal Methods in Energy Informatics (HH), pp. 1–2.

SEFM-2011-Metayer #formal method

Formal Methods as a Link between Software Code and Legal Rules (DLM), pp. 3–18.

SEFM-2011-VassevH #case study #experience #model checking

Developing Model-Checking Mechanisms for ASSL: An Experience Report (EV, MH), pp. 19–34.

SEFM-2011-Pedercini #communication #modelling #policy #process

Models and Communication in the Policy Process (MP), pp. 35–37.

SEFM-2011-HafaiedhGM #distributed #implementation #interactive #multi

Distributed Implementation of Systems with Multiparty Interactions and Priorities (IBH, SG, NM), pp. 38–57.

SEFM-2011-BlechB #coq #semantics #verification

Verification of PLC Properties Based on Formal Semantics in Coq (JOB, SOB), pp. 58–73.

SEFM-2011-BorgstromHJRVPP #calculus #protocol

Broadcast Psi-calculi with an Application to Wireless Protocols (JB, SH, MJ, PR, BV, JÅP, JP), pp. 74–89.

SEFM-2011-BubelHG #formal method #java #specification #string #verification

A Formalisation of Java Strings for Program Specification and Verification (RB, RH, UG), pp. 90–105.

SEFM-2011-CastroKAA #branch #fault tolerance #logic #named #verification

dCTL: A Branching Time Temporal Logic for Fault-Tolerant System Verification (PFC, CK, AA, NA), pp. 106–121.

SEFM-2011-CrespoK #framework #logic #relational

A Machine-Checked Framework for Relational Separation Logic (JMC, CK), pp. 122–137.

SEFM-2011-ParrinoGGF #analysis #bound #data flow #satisfiability #verification

A Dataflow Analysis to Improve SAT-Based Bounded Program Verification (BCP, JPG, DG, MFF), pp. 138–154.

SEFM-2011-VriesK #hoare #logic

Reverse Hoare Logic (EdV, VK), pp. 155–171.

SEFM-2011-EggersRNF #analysis #hybrid #satisfiability

Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods (AE, NR, NSN, MF), pp. 172–187.

SEFM-2011-ErnstSR #analysis #empirical #interactive #proving #theorem proving #verification

Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.

SEFM-2011-FalconeJNBB #component #runtime #verification

Runtime Verification of Component-Based Systems (YF, MJ, THN, MB, SB), pp. 204–220.

SEFM-2011-GarisCR #alloy #diagrams #ocl #specification #uml

Translating Alloy Specifications to UML Class Diagrams Annotated with OCL (AGG, AC, DR), pp. 221–236.

SEFM-2011-HildebrandtMS #declarative #process

Safe Distribution of Declarative Processes (TTH, RRM, TS), pp. 237–252.

SEFM-2011-JacquelBDD #automation #proving #theorem proving #using #verification

Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.

SEFM-2011-MadeiraFMB #approach #hybrid #specification

Hybrid Specification of Reactive Systems: An Institutional Approach (AM, JMF, MAM, LSB), pp. 269–285.

SEFM-2011-MoriLDID #adaptation #configuration management #self

Leveraging State-Based User Preferences in Context-Aware Reconfigurations for Self-Adaptive Systems (MM, FL, CD, PI, SD), pp. 286–301.

SEFM-2011-MorseCNF #bound #ltl #model checking

Context-Bounded Model Checking of LTL Properties for ANSI-C Software (JM, LCC, DN, BF), pp. 302–317.

SEFM-2011-MuscheviciPC #composition #modelling #product line

Modular Modelling of Software Product Lines with Feature Nets (RM, JP, DC), pp. 318–333.

SEFM-2011-NorooziKMW #consistency #testing

Synchronizing Asynchronous Conformance Testing (NN, RK, MRM, TACW), pp. 334–349.

SEFM-2011-OnoHTNH #coq #pipes and filters #specification #using

Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications (KO, YH, YT, NN, MH), pp. 350–365.

SEFM-2011-SoleimanifardGH #composition #named #safety #verification

ProMoVer: Modular Verification of Temporal Safety Properties (SS, DG, MH), pp. 366–381.

SEFM-2011-TschannenFNM #object-oriented #source code #verification

Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques (JT, CAF, MN, BM), pp. 382–398.

SEFM-2011-Boender #component #performance

Efficient Computation of Dominance in Component Systems (JB), pp. 399–406.

SEFM-2011-GouesLM #debugging #verification

The Boogie Verification Debugger (CLG, KRML, MM), pp. 407–414.

SEFM-2011-FadlisyahOA #analysis #formal method #hybrid #modelling #object-oriented

Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude (MF, PCÖ, EÁ), pp. 415–430.

SEFM-2011-CorralC #simulation #towards

Towards an Agent-Based Methodology for Developing Agro-Ecosystem Simulations (JC, DC), pp. 431–446.

SEFM-2011-Pedercini11a #analysis #development #policy

Development Policy Analysis in Mali: Sustainable Growth Prospects (MP), pp. 447–463.

SEFM-2011-Sanchez #using

Using System Dynamics to Assess the Role of Socio-economic Status in Tuberculosis Incidence (MAS), pp. 464–475.

SEFM-2011-TongQ #energy

Energy Consumption and CO2 Emissions of Beijing Heating System: Based on a System Dynamics Model (HT, WQ), pp. 476–485.

SEFM-2011-TongSJ #approach #formal method #information management #process

A Formal Approach to Analysing Knowledge Transfer Processes in Developing Countries (JT, SAS, AEJ), pp. 486–501.