Programme:

Tuesday, September, 9th - Fresco Room
8:30-9:15 Registration
9.15-9:30 iFM Welcome
9:30-10:30 Invited talk (chair: Elvira Albert):

Sophia Drossopoulou. Towards Capability Policy Specification and Verification

10:30-11:00 Coffee break
11:00-12:30 Session 1: Tool Integration 1 (chair: Luigia Petre)

Marcel Vinicius Medeiros Oliveira, Augusto Sampaio and Madiel Conserva. Model-checking Circus State-Rich Specifications.

Martin Hentschel, Stefan Käsdorf, Reiner Hähnle and Richard Bubel. An interactive verification tool meets an IDE.

Andrea Vandin, Mirco Tribastone and Stephen Gilmore. An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems.

12:30-14:00 Lunch
14:00-15:30 Session 2: Tool Integration 2 (chair: John Derrick)

Messaoud Abbas, Choukri-Bey Ben-Yelles and Renaud Rioboo. Modeling UML template classes with FoCaLiZe.

Linas Laibinis, Benjamin Byholm, Inna Pereverzeva, Elena Troubitsyna, Kuan Eeik Tan and Ivan Porres. Integrating Event-B Modelling and Discrete Event Simulation to Analyse Resilience of Data Stores in the Cloud.

Asieh Salehi Fathabadi, Colin Snook and Michael Butler. Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems.

15:30-16:00 Coffee break
16:00-17:30 Session 3: Model Verification (chair: Heike Wehrheim)

Yael Meller, Orna Grumberg and Karen Yorav. Verifying Behavioral UML Systems via CEGAR.

Alvaro Miyazawa and Ana Cavalcanti. Formal refinement in SysML.

Hadrien Bride, Olga Kouchnarenko and Fabien Peureux. Verifying Modal Workflow Specifications using Constraint Solving.

18:30-20:30 Visit of the Rocca and welcome cocktail
Wednesday, September, 10th - Fresco Room
9:30-10:30 Invited talk (chair: Emil Sekerinski):

Helmut Veith. Shape and Content: A database-theoretic perspective on the analysis of data structures

10:30-11:00 Coffee break
11:00-12:30 Session 1: Program Development (chair: Collin Snook)

Johannes Eriksson, Masoumeh Parsa and Ralph-Johan Back. Proofs and Refutations in Invariant-Based Programming.

Dipak L. Chaudhari and Om Damani. Automated Theorem Prover Assisted Program Calculations.

Steve Schneider, Helen Treharne, Heike Wehrheim and David M. Williams. Managing LTL properties in Event-B refinement.

12:30-14:00 Lunch
14:00-15:30 Session 2: Security Analysis (chair: Steve Schneider)

Alessandro Bruni, Michal Sojka, Flemming Nielson and Hanne Riis Nielson. Formal and Experimental Security Analysis of the MaCAN Protocol.

Barbara Kordy, Patrick Schweitzer and Marc Pouly. A Probabilistic Framework for Security Scenarios with Dependent Actions.

John Ramsdell, Daniel Dougherty, Joshua Guttman and Paul Rowe. A Hybrid Analysis for Security Protocols with State.

15:30-16:00 Coffee break
16:00-17:30 Session 3: Concurrency and Control (chair: Helen Treharne)

John Derrick, Graeme Smith and Brijesh Dongol. Verifying linearizability on TSO architectures.

Bogdan Tofan, Gerhard Schellhorn and Wolfgang Reif. A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset.

Lucian Patcas, Mark Lawford and Tom Maibaum. A Separation Principle for Embedded System Interfacing.

18:30-23:00 Visit of "Fattoria Paradiso" and social dinner
Thursday, September, 11th
9:30-10:30 Invited talk - Fresco Room:

Rocco De Nicola. A formal approach to autonomic systems programming: The SCEL Language

10:30-11:00 Coffee break
11:00-12:30 Session 1: Analysis and Transformation (chair: Brijesh Dongol) - Museum Room

Irina Mariuca Asavoae, Mihail Asavoae and Adrian Riesco. Towards a Formal Semantics-Based Technique for Interprocedural Slicing.

Marie-Christine Jakobs, Marco Platzner, Heike Wehrheim and Tobias Wiersema. Integrating Software and Hardware Verification.

Andreas Fürst, Thai Son Hoang, David Basin, Krishnaji Desai, Naoto Sato and Kunihiko Miyazaki. Code Generation for Event-B.

12:30-14:00 Lunch