Dimitra Giannakopoulou, Dominique Méry
Proceedings of the 18th International Symposium of Formal Methods
FM, 2012.

@proceedings{FM-2012,
	address       = "Paris, France",
	doi           = "10.1007/978-3-642-32759-9",
	editor        = "Dimitra Giannakopoulou and Dominique Méry",
	isbn          = "978-3-642-32758-2",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 18th International Symposium of Formal Methods}",
	volume        = 7436,
	year          = 2012,
}

Contents (38 items)

6 ×#formal method
6 ×#using
4 ×#analysis
4 ×#verification
3 ×#algorithm
3 ×#case study
3 ×#performance
3 ×#refinement
3 ×#testing
2 ×#approach

FM-2012-Abadi #formal method #security

Software Security: A Formal Perspective — (Notes for a Talk) (MA), pp. 1–5.

FM-2012-Degani #formal method

Formal Methods in the Wild: Trains, Planes, & Automobile (AD), p. 6.

FM-2012-Wassyng #question #what

Who Are We, and What Are We Doing Here? (AW), pp. 7–9.

FM-2012-AartsHKOV #abstraction #automaton #learning #refinement

Automata Learning through Counterexample Guided Abstraction Refinement (FA, FH, HK, PO, FWV), pp. 10–27.

FM-2012-AlpuenteBFR #named #slicing

Julienne: A Trace Slicer for Conditional Rewrite Theories (MA, DB, FF, DR), pp. 28–32.

FM-2012-AndreFKS #problem #robust #scheduling

IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems (ÉA, LF, UK, RS), pp. 33–36.

FM-2012-AponteCMS #composition #invariant

Maximal and Compositional Pattern-Based Loop Invariants (MVA, PC, YM, MS), pp. 37–51.

FM-2012-AsplundMBCC #approach #coordination #formal method

A Formal Approach to Autonomous Vehicle Coordination (MA, AM, MB, SC, VC), pp. 52–67.

FM-2012-BarringerFHRR #automaton #monitoring #performance #quantifier #runtime #towards

Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors (HB, YF, KH, GR, DER), pp. 68–84.

FM-2012-BauerF #distributed #ltl #monitoring

Decentralised LTL Monitoring (AKB, YF), pp. 85–100.

FM-2012-BenkiraneNSS #algebra #process #using

Measles Epidemics and PEPA: An Exploration of Historic Disease Dynamics Using Process Algebra (SB, RN, ES, CS), pp. 101–115.

FM-2012-CarlierDG #constraints #finite #theorem proving

A Certified Constraint Solver over Finite Domains (MC, CD, AG), pp. 116–131.

FM-2012-ChristakisMW #collaboration #testing #verification

Collaborative Verification and Testing with Explicit Assumptions (MC, PM, VW), pp. 132–146.

FM-2012-CousineauDLMRV #proving

TLA + Proofs (DC, DD, LL, SM, DR, HV), pp. 147–154.

FM-2012-DIppolitoBPU #problem

The Modal Transition System Control Problem (ND, VAB, NP, SU), pp. 155–170.

FM-2012-DormoyKL #component #configuration management #refinement

When Structural Refinement of Components Keeps Temporal Properties over Reconfigurations (JD, OK, AL), pp. 171–186.

FM-2012-ErmisSW #fault #invariant

Error Invariants (EE, MS, TW), pp. 187–201.

FM-2012-GiorginoS #algorithm #correctness #pointer

Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction (MG, MS), pp. 202–216.

FM-2012-HeatherS #framework #modelling

A Formal Framework for Modelling Coercion Resistance and Receipt Freeness (JH, SS), pp. 217–231.

FM-2012-HieronsMN #distributed #order #testing #using

Using Time to Add Order to Distributed Testing (RMH, MGM, MN), pp. 232–246.

FM-2012-HojjatKGIKR #tool support #verification

A Verification Toolkit for Numerical Transition Systems — Tool Paper (HH, FK, FG, RI, VK, PR), pp. 247–251.

FM-2012-JohnsonGMDE #case study #hybrid #verification

Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems (TTJ, JG, SM, RD, RSE), pp. 252–266.

FM-2012-LazarASEMLR #semantics

Executing Formal Semantics with the K Tool (DL, AA, TFS, CE, RM, DL, GR), pp. 267–271.

FM-2012-LinLSDA #automation #composition #verification

Automatic Compositional Verification of Timed Systems (SWL, YL, JS, JSD, ÉA), pp. 272–276.

FM-2012-GrumbergMY #behaviour #model checking #modelling #uml

Applying Software Model Checking Techniques for Behavioral UML Models (OG, YM, KY), pp. 277–292.

FM-2012-MinamideM #analysis #html #parsing #reachability #specification #testing

Reachability Analysis of the HTML5 Parser Specification and Its Application to Compatibility Testing (YM, SM), pp. 293–307.

FM-2012-NedunuriSC #algorithm #performance

Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms (SN, DRS, WRC), pp. 308–325.

FM-2012-NguyenSLDL #analysis

Improved BDD-Based Discrete Analysis of Timed Systems (TKN, JS, YL, JSD, YL), pp. 326–340.

FM-2012-OsaiweranFGR #case study #component #design #experience #formal method #using

Experience Report on Designing and Developing Control Components Using Formal Methods (AO, TF, JFG, BJvR), pp. 341–355.

FM-2012-OwreSS #analysis #automation #cyber-physical

Automatic Dimensional Analysis of Cyber-Physical Systems (SO, IS, NS), pp. 356–371.

FM-2012-PlaggeL #using #validation

Validating B, Z and TLA + Using ProB and Kodkod (DP, ML), pp. 372–386.

FM-2012-RosuS #hoare #logic #reachability

From Hoare Logic to Matching Logic Reachability (GR, AS), pp. 387–402.

FM-2012-SibayUBK

Distribution of Modal Transition Systems (GES, SU, VAB, JK), pp. 403–417.

FM-2012-SongT #detection #model checking #performance #using

Efficient Malware Detection Using Model-Checking (FS, TT), pp. 418–433.

FM-2012-SpasicM #algorithm #formal method #incremental #refinement

Formalization of Incremental Simplex Algorithm by Stepwise Refinement (MS, FM), pp. 434–449.

FM-2012-BeekMS #analysis #named #variability

VMC: A Tool for Product Variability Analysis (MHtB, FM, AS), pp. 450–454.

FM-2012-YangKK #formal method #lightweight #using

Specification-Based Test Repair Using a Lightweight Formal Method (GY, SK, MK), pp. 455–470.

FM-2012-ZhaoZKL #approach #case study #hybrid #industrial

A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example (HZ, NZ, DK, KGL), pp. 471–485.