Thursday, October 6, 2011

Tutorial on the Event-Based B Method,9034

tutorial de Dominique Cansell, Dominique Méry

Documents, Articles about the Worldwide Rail Transport Sector and B Method

The formal method known as B and a sketch for its implementation

B method - An overview through example

The B Method for programmers


ABZ 2012

B Track Chair :
Michael Leuschel , University of Düsseldorf, Germany (

9th International Conference on Integrated Formal Methods (iFM 2012) in conjunction with ABZ 2012, in honor of Egon Boerger's 65th birthday for his contribution to state-based formal methods


9th International Conference on Integrated Formal Methods (iFM 2012)
in conjunction with ABZ 2012, in honor of Egon Boerger's 65th birthday
for his contribution to state-based formal methods

June 18 - 22, 2012 - CNR - Pisa - ITALY

Consiglio Nazionale delle Ricerche
Istituto di Scienza e Tecnologie dell'Informazione ``A. Faedo''
Formal Methods && Tools Lab.
Via Moruzzi 1 - 56124 Pisa

Applying formal methods may involve the modeling of different aspects
of a system that are expressed through different paradigms.
Correspondingly, different analysis techniques will be used to examine
differently modeled system views, different kinds of properties, or
simply in order to cope with the sheer complexity of the system.
The iFM conference series seeks to further research into the
combination of (formal and semi-formal) methods for system development,
regarding modeling and analysis, and covering all aspects from language
design through verification and analysis techniques to tools and their
integration into software engineering practice   Areas of interest
include but are not limited to:

- Case Studies;
- Experience reports;
- Formal and semiformal modelling notations;
- Integration of formal methods into software engineering practice;
- Logics;
- Model checking;
- Model transformations;
- Semantics;
- Static Analysis;
- Refinement;
- Theorem proving;
- Tools;
- Type Systems;
- Verification

iFM 2012 solicits high quality papers reporting research results and/or
experience reports related to the overall theme of method integration.
The conference proceedings will be published by Springer Lecture Notes
in Computer Science series. All papers must be original, unpublished,
and not submitted for publication elsewhere. All submissions must be
in PDF format, using the Springer LNCS style files; we suggest to use
the LaTeX2e package (the llncs.cls class file, available in
and the typeinst.dem available in as a template for your
contribution).  Submissions should be made using the iFM 2012 Easychair
web site. Papers should not exceed 15 pages in length. Each paper will
undergo a thorough review process.

All accepted papers must be presented at the conference. Their
authors must be prepared to sign a copyright transfer statement.
At least one author of each accepted paper must register to the
conference by the early date indicated by the organizers, and
present the paper.

Paper submission: January 14, 2012
Paper notification: March 1, 2012
Final version paper: March 20, 2012

Egon Boerger, University of Pisa, Italy
Muffy Calder, University of Glasgow, United Kingdom
Ian J. Hayes, University of Queensland, Australia

John Derrick, University of Sheffield, United Kingdom
Stefania Gnesi, CNR-ISTI, Italy

Diego Latella, CNR-ISTI, Italy
Helen Treharne, University of Surrey, United Kingdom

Alessandro Fantechi, Universita' di Firenze, Italy

Maurice ter Beek, CNR-ISTI, Italy

Maurice ter Beek, CNR-ISTI, Italy
Angelo Gargantini, Universita' di Bergamo, Italy

Marc Benveniste, STMicroelectronics Rousset, France
Eerke Boiten, University of Kent, UK
Jonathan Bowen, Museophile Limited, UK
Jim Davies, Oxford University, UK
John Derrick, University of Sheffield, UK
Jin Song Dong, National University of Singapore
Kerstin Eder, University of Bristol, UK
Alessandro Fantechi, Univ. Florence & CNR/ISTI, Italy
John Fitzgerald, University of Newcastle, UK
Andy Galloway, University of York, UK
Einar Broch Johnsen, University of Oslo, Norway
Rajeev Joshi, NASA Jet Propulsion Laboratory, USA
Diego Latella, CNR/ISTI, Italy
Michael Leuschel, University of Duesseldorf, Germany
Michele Loreti, University of Florence, Italy
Dominique Mery, Nancy University and LORIA, France
Stephan Merz, INRIA Nancy and LORIA, France
Alexandre Mota, CIn-UFPE, Brasil
Flemming Nielson, Technical University of Denmark
Luigia Petre, Abo Akademi University, Turku, Finland
David Pichardie, INRIA Rennes, France
Thomas Santen, Microsoft Research, Aachen, Germany
Steve Schneider, University of Surrey, UK
Kaisa Sere, Abo Akademi University, Turku, Finland
Graeme Smith, University of Queensland, Australia
Kenji Taguchi, AIST, Japan
Helen Treharne, University of Surrey, UK
Mirco Tribastone, LMU, Germany
Marina Walden, Abo Akademi Univ., Turku, Finland
Heike Wehrheim, University of Paderborn, Germany
Kirsten Winter, University of Queensland, Australia

This call for papers and additional information about the conference
can be found at
For information regarding the conference you can contact:

Rodin User and Developer Workshop, 27-29 February 2012, Fontainebleau, France

Rodin User and Developer Workshop, 
27-29 February 2012, Fontainebleau,

Event-B is a formal method for 
system-level modelling and analysis. The
Rodin Platform is an Eclipse-based 
toolset for Event-B that provides
effective support for modelling 
and automated proof. The platform is open
source and is further extendable with 
plug-ins. A range of plug-ins have
already been developed including ones
that support animation, model
checking and UML-B.

The first Rodin User and Developer
Workshop was held at the University of
Southampton while the second took place 
at the University of Düsseldorf in
2010. The 2012 workshop will be part 
of the DEPLOY Federated Even hosted
by the LACL laboratory at IUT Sénart-Fontainebleau.
Fontainebleau is
within easy reach of Paris:

If you are interested in giving 
a presentation at the Rodin workshop, send
a short abstract (1 or 2 pages PDF) 
to by
        16 January 2012.

Attendance at the DEPLOY Federated 
Event (including the Rodin Workshop) is
open to all.


Michael Butler, University of Southampton
Stefan Hallerstede, University of Aarhus
Thierry Lecomte, ClearSy
Michael Leuschel, University of Düsseldorf
Alexander Romanovsky, Newcastle University
Laurent Voisin, Systerel

Une Deuxième Révolution Galiléenne

Ca se passe le vendredi prochain 7 octobre à 15h30
en salle i001, département de
mathématiques de l'Université d'Angers.
Cela peut intéresser les chercheurs, mais aussi les enseignants !

Une Deuxième Révolution Galiléenne

Gilles Dowek (INRIA)

L'introduction d'un nouveau concept
scientifique permet souvent de
donner de nouvelles réponses à des
questions anciennes qui n'avaient
jusqu'alors reçu que des réponses 
imparfaites. Par exemple,
l'introduction des notions d'atome 
et molécule a permis de donner de
nouvelles réponses aux questions/ 
"qu'est-ce que l'oxygène ?","qu'est-ce
que l'eau ?", "qu'est-ce qu'une 
réaction chimique ?",/.... Cet exposé
présentera quelques questions qui
ont trouvé de nouvelles réponses
depuis que nous comprenons mieux 
la notion d'algorithme : "/qu'est-ce
qu'un aéroport ?", "qu'est-ce 
qu'un nombre entier ?", "qu'est-ce qu'une
démonstration mathématique ?",
"qu'est-ce qu'une théorie mathématique
?", "qu'est-ce qu'une loi physique ?",/
... La prise de conscience du
caractère algorithmique de ces 
objets scientifiques nous amène à
considérer de nouveaux langages 
pour les décrire. Cette révolution, dans
le langage dans lequel la science
s'écrit, peut-être comparée à la
révolution qui s'est produite, 
au début du XVIIe siècle, quand le
langage mathématique a commencé
à être utilisé pour décrire des
phénomènes physiques.