Important dates

abstracts: May 21
full papers: May 28
notification: July 4
final version: July 23
early registration: Sept 15
conference: October 11-14

Contact

ifm2010@loria.fr

Conference Program    ( download as PDF, but note changes below)

Monday, October 11, 2010

09:30 - 17:00 WTS 2010: Workshop on Formal Methods for Web Data Trust and Security
09:00 - 12:30 Tutorial: Verification of C# programs using Spec# and Boogie 2 ( slides, examples)
Rosemary Monahan, National University of Ireland
10:30 - 10:50
12:45 - 14:00
15:20 - 15:40
coffee and lunch breaks
14:00 - 17:30 Tutorial: The TLA+ Proof System ( slides, examples)
Denis Cousineau, MSR-INRIA Joint Centre, Saclay, Stephan Merz, INRIA Nancy & LORIA

Tuesday, October 12, 2010

08:30 Registration
Opening session  (chair: Dominique Méry)
09:15 Opening of iFM 2010
09:30 Collaborative Modelling and Co-Simulation in the Development of Dependable Embedded Systems
John Fitzgerald, School of Computer Science, Newcastle University
 
10:30 Coffee break
Model Transformations I  (chair: Helen Treharne)
11:00 Systematic translation rules from ASTD to Event-B
Jérémy Milhau, Marc Frappier, Frederic Gervais, Régine Laleau
11:30 Multiformalism and transformation inheritance for dependability analysis of critical systems
Stefano Marrone, Camilla Papa, Valeria Vittorini
12:00 Full Semantics Preservation in Model Transformation – A Comparison of Proof Techniques
Mathias Hülsbusch, Barbara König, Arend Rensink, Maria Semenyak, Christian Soltenborn, Heike Wehrheim
 
12:45 Lunch
Probabilistic and Real-Time Systems  (chair: Steve Schneider)
14:15 Satisfaction Meets Expectations: Computing Expected Values of Probabilistic Hybrid Systems with SMT
Martin Fränzle, Tino Teige, Andreas Eggers
14:45 Towards Probabilistic Modelling in Event-B
Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis
15:15 Verification Architectures: Compositional Reasoning for Real-time Systems
Johannes Faber
 
15:45 Coffee break
Verification I  (chair: Heike Wehrheim)
16:15 Symbolic Model-Checking of Optimistic Replication Algorithms
Hanifa Boucheneb, Abdessamad Imine, Manal Najem
16:45 A Logical Framework to Deal with Variability
Patrizia Asirelli, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi
17:15 From Operating-System Correctness to Pervasively Verified Applications
Matthias Daum, Norbert Schirmer, Mareike Schmidt
 
19:00 Welcome Reception at Musée Lorrain

Wednesday, October 13, 2010

Invited talk  (chair: Stefania Gnesi)
09:30 Programming with Miracles
Rajeev Joshi, Laboratory for Reliable Software, NASA Jet Propulsion Laboratory
 
10:30 Coffee break
Refinement  (chair: Bernard Boigelot)
11:00 Creating sequential programs from Event-B models
Pontus Boström
11:30 A CSP approach to Control in Event-B
Steve Schneider, Helen Treharne, Heike Wehrheim
12:00 Translating Pi-Calculus into LOTOS NT
Radu Mateescu, Gwen Salaün
 
12:45 Lunch
Verification II  (chair: Martin Steffen)
14:15 Integrating Implicit Induction Proofs into Certified Proof Environments
Sorin Stratulat
14:45 Automatic Verification of Parametric Specifications with Complex Topologies
Johannes Faber, Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans
15:15 Adding Change Impact Analysis to the Formal Verification of C Programs
Serge Autexier, Christoph Lüth
 
15:45 Coffee break
Program Analysis  (chair: Martin Fränzle)
16:15 A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs
Aleksandar Dimovski
16:45 Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
Javier de Dios, Manuel Montenegro, Ricardo Peña
17:15 Safe Commits for Transactional Featherweight Java
Thi Mai Thuong Tran, Martin Steffen
 
19:30 Conference Dinner, Hôtel de Ville, Place Stanislas

Thursday, October 14, 2010

Invited talk  (chair: Stephan Merz)
09:30 Invited talk
On Model Checking Techniques for Randomized Distributed Systems
Christel Baier, Chair of Algebraic and Logical Foundations of Computer Science, TU Dresden
 
10:30 Coffee break