The B method : from Research to Teaching

B et cryptographie

2012-01-30T18:00:00.002+01:00

http://www.scd.uhp-nancy.fr/docnum/SCD_T_2010_0034_BENAISSA.pd

FM 2012

2012-01-30T13:32:00.000+01:00

CALL FOR PAPERS  FM 2012

*********************************************
18TH INTERNATIONAL SYMPOSIUM

 ON FORMAL METHODS
August  27 - 31, 2012
CNAM, Paris, France
http://fm2012.cnam.fr
*********************************************

*IMPORTANT DATES:

Submission: March 5th, 2012
Notification: May 7th, 2012
Camera ready: June 4th, 2012

原书名： The B-Book:Assigning Programs to Meanings

2011-11-03T15:28:00.000+01:00

点击看大图

定价：￥57.00
普通会员：￥51.30
1-3星会员：￥50.16
4-5星会员：￥48.45

团购急调缺货预定

基本信息

原书名： The B-Book:Assigning Programs to Meanings
原出版社： Cambridge University Press

作者： [美]Jean-Raymond Abrial, J.-R. Abrial [作译者介绍]
译者：裘宗燕
丛书名： 国外计算机科学教材系列
出版社：电子工业出版社
ISBN：7505393391
上架时间：2004-7-1
出版日期：2004 年6月
开本：16开
页码：526
版次：1-1

Techniques industrielles de modélisation formelle pour le transport

2011-11-02T20:13:00.000+01:00

Introduction - Jean-Louis BOULANGER
1. Une approche innovante et une aventure humaine au service
de la sécurité ferroviaire - Sylvain FIORONI
2. SAET-METEOR - Jean-Louis BOULANGER
3. Preuve de propriétés globales à l’aide de l’outil de preuve SIMULINK
DESIGN VERIFIER - Véronique DELEBARRE, Jean-Frédéric ETIENNE
4. Démonstration de la sécurité d’une application ferroviaire de signalisation
en mode nominal et en modes dégradés par la preuve formelle
Jean-Marc MOTA, Evguenia DMITRIEVA, Amel MAMMAR, Paul CASPI,
Salimeh BEHNIA, Nicolas BRETON, Pascal RAYMOND
5. Utilisation de la preuve formelle dans le CBTC (OCTYS)
Christophe TREMBLIN, Pierre LESOILLE, Omar REZZOUG
6. Validation d’automatismes ferroviaires de sécurité à base de réseaux
de Petri - Marc ANTONI
7. ERTMS Formal Specs : un langage dédié pour la formalisation
des spécifications pour le développement d’unité bord ERTMS
Laurent FERIER, Stanislas PINTE, Darius BLASBAND, Svitlana LUKICHEVA
8. Synthèse et conclusions - Jean-Louis BOULANGER
Glossaire
Bibliographies. Index

http://www.lavoisier.fr/livre/h3230.html

Fourth NASA Formal Methods Symposium

2011-11-02T20:10:00.002+01:00

SECOND CALL FOR PAPERS

NFM 2012

Fourth NASA Formal Methods Symposium

Norfolk, Virginia, USA
April 3 - 5, 2012

http://shemesh.larc.nasa.gov/nfm2012/

nasa-nfm2012@mail.nasa.gov

Tutorial on the Event-Based B Method

2011-10-06T12:12:00.000+02:00

http://www.needocs.com/document/academique-cours-mathematiques-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

2011-10-06T12:09:00.002+02:00

http://www.fersil-railway.com/php/documents-en.php

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

2011-10-06T12:08:00.001+02:00

http://www.ewaromanowicz.com/academics/B_method_An_overview_through_example.pdf

B method - An overview through example

2011-10-06T12:04:00.002+02:00

http://www.ewaromanowicz.com/academics/B_method_An_overview_through_example.pdf

The B Method for programmers

2011-10-06T11:41:00.002+02:00

http://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_programmers_%28part_1%29/

Composys

2011-10-06T11:32:00.000+02:00

http://www.composys.fr/

ABZ 2012

2011-10-06T10:32:00.000+02:00

http://ifm-abz.isti.cnr.it/page22/abzindex.html

B Track Chair :
Michael Leuschel , University of Düsseldorf, Germany (leuschel@cs.uni-duesseldorf.de)

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

2011-10-06T10:27:00.000+02:00

PRELIMINARY
CALL FOR PAPERS

**********************************************************************
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        http://ifm.isti.cnr.it

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

OBJECTIVES AND SCOPE
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


SUBMISSION GUIDELINES
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 llncs2e.zip
and the typeinst.dem available in typeinst.zip 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.


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


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


ABZ - iFM 2012 GENERAL CHAIRS
John Derrick, University of Sheffield, United Kingdom
Stefania Gnesi, CNR-ISTI, Italy

iFM PROGRAMME COMMITTEE CHAIRS:
Diego Latella, CNR-ISTI, Italy
Helen Treharne, University of Surrey, United Kingdom

FINANCE CHAIR
Alessandro Fantechi, Universita' di Firenze, Italy

ORGANIZING COMMITTEE CHAIR
Maurice ter Beek, CNR-ISTI, Italy

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

PROGRAM COMMITTEE
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 http://ifm.isti.cnr.it
For information regarding the conference you can contact:
iFM2012@isti.cnr.it

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

2011-10-06T10:25:00.000+02:00

Rodin User and Developer Workshop,

27-29 February 2012, Fontainebleau,
France

http://wiki.event-b.org/index.php/Rodin_Workshop_2012

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:

http://www.bmethod.com/php/federated-event-2012-en.php


If you are interested in giving

a presentation at the Rodin workshop, send
a short abstract (1 or 2 pages PDF)

to rodin@ecs.soton.ac.uk by
        16 January 2012.


Attendance at the DEPLOY Federated

Event (including the Rodin Workshop) is
open to all.

Organisers

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

2011-10-06T10:22:00.000+02:00

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 !
Colin

=====================================
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.

Les Journées Scientifiques 2011 de l'Université de Nantes

2011-06-05T22:07:00.000+02:00

Ont lieu demain. La conférence The B Method : from Research to Teaching n'aura pas lieu cette année.

RDV aux conférences grand-public

15h00-16h00 : Conférence « Greffer des organes d'animaux sur l'homme : rêve ou réalité ?" par Jean-Paul SOULILLOU, Professeur à l'Université de Nantes, Praticien Hospitalier au CHU de Nantes

16h15-17h00 : Conférence « Pourquoi une éthique du soin est-elle nécessaire aujourd'hui ?" par Fabienne BRUGÈRE, Philosophe, Professeur à l'Université Montaigne-Bordeaux III, Présidente du Conseil de développement durable de la Communauté Urbaine de Bordeaux

17h00-18h00 : Table ronde sur le thème des nouvelles technologies en santé. Échange avec le public en présence de :

Jean-Paul SOULILLOU
Fabienne BRUGÈRE
Jean-Paul GALMICHE, Professeur à l'Université de Nantes, Praticien hospitalier au CHU de Nantes, spécialiste d'hépato-gastroentérologie.

10h30 - 18h00 : Nous vous invitons également à venir visiter les stands et expositions dans la grande halle de la Cité Nantes Events Center (laboratoires, expositions, vidéos, formations...).

WWV 2011 Automated Specification and Verification of Web Systems

2011-02-17T18:34:00.002+01:00

First Call for Papers

WWV 2011
Automated Specification and Verification of Web Systems
7th International Workshop
(as part of DisCoTec'11)

http://rap.dsi.unifi.it/wwv2011/

June 9, 2011 - Reykjavik, Iceland

********************************************************


IMPORTANT DATES

Abstract Submission                        March 28, 2011
Full Paper Submission                        April 4, 2011
Acceptance Notification                              May 3, 2011
Camera Ready (pre-proceedings)                May 30, 2011
Workshop                                June 9, 2011
Camera Ready (post-proceedings)                July 4, 2011

Workshop B 2011, colocated with FM 2011, Limerick, Ireland, june, 21, 2011

2011-02-17T18:33:00.000+01:00

http://membres-liglab.imag.fr/idani/BWorkshop/index.html

IMPORTANT DATES
Abstract submission         March 3, 2011
Paper submission         March 10, 2011
Acceptance notification         April 12, 2011
Final version         May 4, 2011
Workshop         June 21, 2011

the release of ProB for Rodin 2.1

2011-02-13T14:12:00.001+01:00

We are happy to announce the release of 
    ProB for Rodin 2.1

Numerous improvements went into the latest release:
- constraint-based deadlock checker: finds counter-examples

to the deadlock freedom
PO using constraint-solving
- improved kernel with improved constraint solving

(in particular improved boolean
constraint solver)
- ProB can now efficiently solve integer constraints

using the finite domain solver
CLP(FD) (you can turn this feature on in

the Preferences Dialog)
- improved LTL model checker with new counter-example display
- new, improved version of BMotionStudio to generate

graphical visualisations of
your models
- automatic record detection (when defining closed

records using Records plug-in or
manually using bijections on Cartesian products)
- 64-bit version of ProB for Mac OS X (performance

improvement; less hash collisions
in model checking; larger range for the integer

constraint solver; ...)
- and many more.

To install ProB, first download Rodin 2.1,

choose Help -> Install New Software and
simply choose the pre-configured ProB update site.
More detailed installation instructions and a brief

tutorial can be found here:
 http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Rodin_First_Step

We have also released the new version 1.3.3 of ProB

Classic, a version of ProB with
a Tcl/Tk interface.
It can be obtained at:

http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download
ProB Classic, is a stand-alone application but can

be started automatically from
within Rodin by setting the ProB Classic preference.
ProB Classic provides some features which are not

yet available in the ProB for
Rodin version
(graphical visualisation of the state space,

debugging of axioms with unsat core
computation, CSP support...).

Kind regards,
The ProB Team from Düsseldorf
http://www.stups.uni-duesseldorf.de/ProB/

Have we learned from the Wasa disaster ? J.R. Abrial

2011-02-13T14:10:00.000+01:00

http://videotorium.hu/en/recordings/details/1674,Have_we_learned_from_the_Wasa_disaster_

Conference, 2006. September 19 - 20.
http://www.jaist.ac.jp/~bjorner/ae-is-budapest/

The AE/IS `Charles Simonyi' Symposium: Grand Challenges of Informatics is a major event. Some 14 of the nest computer scientists will, over two days, present challenges within areas of 100% trustworthy software, quantum computing, biocomputing, economics and game theory, and the relations between informatics and mathematics. Thanks to Dr. Simonyi's donation the event will host some 40 young scientists from Central and Eastern European countries.

FM 2011: 17TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

2010-12-12T11:25:00.000+01:00

http://fm2011.lero.ie

June 20 - 24, 2011

Lero, Limerick, Ireland

Structures de données et méthodes formelles, Marc Guyomard, Springer

2010-11-30T09:58:00.002+01:00

Ce livre porte sur l’étude des structures de données, à savoir des constituants logiciels dont la qualité conditionne le bon fonctionnement et l’efficacité des applications informatiques. L’originalité de cet ouvrage réside essentiellement dans le lien qu’il établit avec la discipline des méthodes formelles pour le génie logiciel. Il montre comment il est possible de calculer les opérations qui accompagnent une structure de données à partir d’une spécification rigoureuse. L’auteur adopte à la fois une perspective historique et une démarche fonctionnelle. La première partie de l’ouvrage présente les bases de la discipline : la théorie des ensembles, l’étude de structures intermédiaires (listes, arbres, sacs), et l’analyse des algorithmes. La seconde partie se focalise sur l’étude approfondie de cinq structures de données typiques : les ensembles simples, les ensembles composites, les files simples, les files de priorité, et les tableaux flexibles. Des exercices accompagnent chaque chapitre.

1st Edition., 2011, 426 p., Broché
ISBN: 978-2-8178-0199-5

à paraître: mars 2011
http://www.springer.com/computer/book/978-2-8178-0199-5?changeHeader
http://www.irisa.fr/cordial/mguyomar/guyomard-15-09-05.htm

Décès de Michel Sintzoff

2010-11-29T21:01:00.001+01:00

http://www.ae-info.org/ae/User/Sintzoff_Michel

On m'apprend :

" C'est avec une très grande tristesse que j'ai appris ce lundi le décès de Michel Sintzoff.
Michel était une personnalité exceptionnelle de la recherche en Informatique. Sa curiosité scientifique l'avait amené à travailler dans de nombreux domaines de notre discipline (Langages, Intelligence Artificielle, Bases de Données, Génie Logiciel, Informatique Distribuée,...).

Il avait des amis partout dans le monde, et donc naturellement en France (à Paris, Toulouse, Nancy, Grenoble,...).Beaucoup se souviendront de son ouverture d'esprit, de la pertinence de ses remarques et de son rire inimitable. "

FSEN '11

2010-10-20T09:56:00.000+02:00

Fourth International Conference on 
Fundamentals of Software Engineering 2011 
Theory and Practice 
(FSEN '11) 

http://fsen.ir/2011/fsen.ir/2011 

Tehran, Iran 
April 20-22, 2011

The Space and Motion of Communicating Agents

2010-10-20T08:39:00.000+02:00

Robin Milner, Cambridge, 2009
http://www.cambridge.org/gb/knowledge/isbn/item2427683/?site_locale=en_GB

http://www.cl.cam.ac.uk/archive/rm135/
http://www.cl.cam.ac.uk/misc/obituaries/milner/

Cours et exercices corrigés d'algorithmique

2010-10-20T08:35:00.000+02:00

Vérifier, tester et concevoir des programmes en les modélisant,
Jacques Julliand
Vuibert, 2010

Utilise la notation B.
http://www.vuibert.com/livre33767.html

Death of Jean-Claude Laprie

2010-10-20T08:28:00.001+02:00

Dear colleague,

With deep sadness we bring you the news of Jean-Claude

passing away after a battle with cancer,

Saturday night (October 17).
The funeral arrangements are not settled yet.

More information will be provided when
available.

TSF group at LAAS

Méthodes de spécification de systèmes temps réel en B

2010-10-07T12:07:00.002+02:00

http://www.cert.fr/feria/svf/FAC/2004/Papiers/I2.pdf

THE PROGRAMMING LANGUAGE B

2010-10-07T11:51:00.002+02:00

"B is a computer language designed by D. M. Ritchie and K. L.
Thompson, for primarily non-numeric applications such as system
programming. These typically involve complex logical decisionmaking,
and processing of integers, characters, and bit strings.
On the H6070 TSS system, B programs are usually much easier to
write and understand than assembly language programsj and object
code efficiency is almost as good. Implementation of simple TSS
subsystems is an especially appropriate use for B."
http://minnie.tuhs.org/Mirrors/Dennis/btut.pdf

B vs. Coq to prove a Garbage Collector

2010-10-07T11:46:00.000+02:00

http://www-sop.inria.fr/everest/personnel/Lilian.Burdy/b085.pdf

Processus de validation basée sur la notion de propriété

2010-10-07T11:43:00.002+02:00

http://www.rennes.supelec.fr/sic/REUNIONS/SdF/.../Gallardo.ppt

Formal Methods in Safety-Critical Railway Systems

2010-10-07T11:36:00.002+02:00

http://deploy-eprints.ecs.soton.ac.uk/8/1/fm_sc_rs_v2.pdf

Vers une méthodologie de Validation et de Vérification multi-formelle des Interfaces Utilisateurs en milieu industriel

2010-10-07T11:35:00.002+02:00

http://www.cert.fr/tis/theses/jthese_05/ressources/articles/cortier.pdf

The Development of a Probabilistic B-Method and a Supporting Toolkit

2010-10-07T11:33:00.002+02:00

http://www.cse.unsw.edu.au/~carrollm/probs/Papers/Hoang-05a.pdf

Les bases du langage B

2010-10-07T11:32:00.002+02:00

http://www.lri.fr/~paulin/B/poly002.html

A formal specification of the javaByte code semantics using the B method

2010-10-07T11:29:00.002+02:00

http://www.gemplus.com.mx/smart/rd/publications/pdf/CL99ecop.pdf

Using B Method to Formalize the Java Card Runtime Security Policy for a Common Criteria Evaluation

2010-10-07T11:27:00.002+02:00

http://www.gemplus.com/smart/rd/publications/pdf/MT00bjav.pdf

How to formally specify the Java Bytecode semantics using the B method

2010-10-07T11:26:00.002+02:00

http://www.imamu.edu.sa/dcontent/IT_Topics/java/lisbonne.pdf

Formalisation and Veri¯cation of the GlobalPlatform Card Speci¯cation Using the B Method

2010-10-07T11:25:00.002+02:00

http://software.imdea.org/~szanella/Zanella.2006.CASSIS.pdf

ProB: An Automated Analysis Toolset for the B Method

2010-10-07T11:24:00.002+02:00

http://www.stups.uni-duesseldorf.de/publications/overview_final.pdf

Applying the B Formal Method to the Bossa Domain-Specific Language

2010-10-07T11:23:00.002+02:00

http://www.diku.dk/hjemmesider/ansatte/julia/Lawall_nwpt05.pdf

Cooperation Between the B Method and the Automata Theory to Check the Component Interoperability

2010-10-07T11:22:00.002+02:00

http://www.iist.unu.edu/www/docs/techreports/reports_old/report344/15-Chouali.pdf

PBS, support of the B Method in PVS, Cesar Munoz, SRI

2010-10-07T11:17:00.000+02:00

http://research.nianet.org/~munoz/PBS/pbs.pdf

Component-based Development using the B method

2010-10-07T11:16:00.000+02:00

http://hal.archives-ouvertes.fr/hal-00105041/

Tutorial on the B method

2010-10-07T11:03:00.002+02:00

http://hal.archives-ouvertes.fr/docs/00/09/28/46/PDF/tutorialforte2006mery.pdf

The B Method for Programmers

2010-10-07T11:00:00.002+02:00

http://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_programmers_%28part_1%29/

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

2010-10-07T10:58:00.000+02:00

Antti-Juhani Kaijanaho
Master's Thesis
in Information Technology (Software Engineering)
20th December 2002
http://users.jyu.fi/~antkaij/gradu.pdf

Program Development by Refinement: Case Studies Using the B Method (Formal Approaches to Computing and Information Technology (FACIT))

2010-10-07T10:54:00.000+02:00

Emil Sekerinski (Editor), Kaisa Sere (Editor)
http://www.amazon.com/reader/1852330538?_encoding=UTF8&ref_=sib_dp_pt#reader-link

Security of Computer Architectures, Jean-Louis Boulanger

2010-10-07T10:50:00.000+02:00

Relié: 512 pages
Editeur : ISTE Ltd and John Wiley & Sons Inc (16 juillet 2010)
Langue : Anglais
ISBN-10: 184821197X
ISBN-13: 978-1848211971
http://eu.wiley.com/WileyCDA/WileyTitle/productCd-184821197X.html?cid=RSS_WILEY2_ENGINEERING

Le dernier livre d'Umberto Eco en français

2010-10-07T09:40:00.000+02:00

http://www.bibliosurf.com/De-l-arbre-au-labyrinthe

Dall'albero al labirinto. Studi storici sul segno e l'interpretazione

Studi storici sul segno e l’interpretazione

http://bompiani.rcslibri.corriere.it/libro/5902_dall_albero_al_labirinto_studi_eco.html

Autore: Umberto Eco

Titolo: Dall'albero al labirinto. Studi storici sul segno e l'interpretazione

Editore: BOMPIANI

Collana: STUDI E STRUMENTI

Pagine: 640

Prezzo: 25,00 euro

Anno prima edizione: 2007

ISBN: 45259029

FM 2011 (20-24 June 2011, Limerick, Ireland): Call for Tutorials

2010-10-07T09:25:00.003+02:00

 http://www.lero.ie/fm2011/

Workshop on B Dissemination

2010-06-15T16:52:00.002+02:00

Workshop on B Dissemination

November 8-9, 2010
Natal, Brazil
http://www.bmethod.com/php/conference-sbmf-2010-en.php

Satellite event of SBMF 2010 <

http://sbmf2010.dimap.ufrn.br/>


    Presentation

This B / event-B workshop is organized on behalf of the

DEPLOY project 
<http://www.deploy-project.eu/>.

Its objectives are to present current 
status and ongoing research
and development related to B and

event B languages and tools, as well as 
applications to industry size problems.
Topics addressed by the workshop are many,

including but not limited to:

* Tool development (language extensions,

external provers, code
generation, etc.)
* Modelling challenges (real time properties, probabilistic
refinement, design patterns, high order logic, etc.)
* Deployment (methodology, cases-studies, return of experience,
scaling up, etc.)
* Teaching and training

Researchers are invited to contribute to the

second day of the workshop 
through an open call for papers.


    Program

The workshop lasts 2 days:

* The first day is devoted to DEPLOY speakers.

General presentation
of the project and tools will be sided by

focused talks on
scientific/technical
matters (modelling time, code generation,

model animation, model
checking, etc.) that are being researched in DEPLOY.
Reports on industrial applications (space,

railways, automotive,
information systems, etc.) will complete the day.
* The second day is open to any presenter,

through an international
 call for papers. Expected contributions would

range from theoretical research to
practical applications of B/event B.

Submissions are handled by
the programme committee.

The workshop is collocated with the SBMF

conference (Monday and 
Tuesday), at the Imira Plaza hotel &lt

;http://www.imiraplaza.com.br/>.


Important Dates
* Paper submission deadline: 30 July 2010
* Notification of acceptance/rejection:

06 September 2010
* Workshop in Natal, Brazil: 08-09 November 2010


Submission and attendance

We anticipate a rich exchange of ideas and discussions

during this event. Submissions are welcomed on any

subject that falls within the main issues.
Papers should be around 6 pages in ENTCS style.

All papers must be submitted in PDF format,

following the instructions at the WOBD'10 submission

site, handled by EasyChair:
http://www.easychair.org/conferences/?conf=wobd2010.

All accepted papers should be presented during the workshop.

Committees
 Workshop Chair:
* Thierry Lecomte <

mailto:thierry.lecomte@clearsy.com> (ClearSy)


 Program Committee:

* Michael Butler (University of Southampton, UK)
* Clif Jones (University of Newcastle, UK)
* Jérôme Phalampin (Siemens Transportation Systems, France)
* Lilian Burdy (ClearSy, France)
* David Basin (ETH Zurich, Switzerland)
* Michael Leuschel (University of Dusseldorf, Germany)
* Mathieu Clabaut (Systérel, France)
* Christophe Ponsard (CTIC, Belgium)
* Elena Troubitsyna (University of Turku, Finland)
* Rainer Gmehlich (Bosch, Germany)
* Aryldo Russo (AeS, Brazil)

B方法 , The B Book in chinese

2010-06-08T14:28:00.002+02:00

http://www.china-pub.com/19779

基本信息

原书名： The B-Book:Assigning Programs to Meanings
原出版社： Cambridge University Press

作者： [美]Jean-Raymond Abrial, J.-R. Abrial [作译者介绍]
译者：裘宗燕[同译者作品]
丛书名： 国外计算机科学教材系列
出版社：电子工业出版社
ISBN：7505393391
上架时间：2004-7-1
出版日期：2004 年6月
开本：16开
页码：526
版次：1-1
所属分类：计算机 > 软件工程及软件方法学 >

综合

教材 > 研究生/本科/专科教材 > 工学 >

计算机

教材 > 计算机教材 > 本科 /研究生 > 计算机专业 > 计算机专业课程 >

软件工程

General-Service Ballistic Computer Programming Based on B-Method

2010-06-08T14:22:00.000+02:00

"Formal methods offer the promise of significant improvement on quality and reliability of critical embedded software. B-Method is employed to develop general-service ballistic computer programs in the paper, each of which can be adapted to a family of service/weapon-specific ballistic computers. Based on the structuring mechanisms of B-method, a unified approach is proposed to systematically control the complexity of ballistic parameters in the process of type and operation refinement, and ultimately a series of high reliable, reusable, and scalable programs are produced. Experiences with the application of the method and tools are also discussed."
http://d.wanfangdata.com.cn/Periodical_bgxb-e200603005.aspx

Formal development of a washing machine controller by using formal design patterns

2010-06-08T12:42:00.000+02:00

http://portal.acm.org/citation.cfm?id=1519454&CFID=93110173&CFTOKEN=11513284

Event Model Decomposition

2010-06-08T12:35:00.000+02:00

http://wiki.event-b.org/index.php/Event_Model_Decomposition

The papers and the slides of the conference 2010 are here ...

2010-06-08T12:30:00.000+02:00

http://www.lina.sciences.univ-nantes.fr/apcb/BDayNantes2010/program.html

L'Université de Nantes a 550 ans cette année

2010-05-10T15:40:00.000+02:00

ttp://www.archivesdefrance.culture.gouv.fr/action-culturelle/celebrations-nationales/brochure-2010/vie-politique/universite-de-nantes/

On line registration for the 2010 Conference

2010-05-09T18:38:00.002+02:00

http://www.lina.sciences.univ-nantes.fr/apcb/BDayNantes2010/registration.html

Programme of the 2010 conference

2010-05-09T18:37:00.002+02:00

http://www.lina.sciences.univ-nantes.fr/apcb/BDayNantes2010/programme_tfmb2010.html

8:30-9:00 Welcome

9h00 – 10h00 : Conférence invitée / Invited Talk
Formal proofs of local computation systems, using Rodin and/or Coq

Pierre Castéran, Université de Bordeaux, LaBRI, FR

10h00 – 10h15 : Pause / Break

10h15 – 10h50 : Teaching Logic Proofs for Formal Aspects

David Cumbor, Bill Stoddart, Steve Dunne, University of Teesside, UK

10h50 – 11h25 : Using the B Method in Teaching Software Technology at Eötvös Lorànd University

Akos Fothi, Zoltan Istenès, Eötvös Lorànd University, HU

11h25- 11h40 Pause / Break

11h40 – 12h15 : New Features of Atelier B 4.0

Thierry Lecomte, ClearSy, Aix-en-Provence, FR

12h15-12h50 : B for Children

Mireille Samia, University of Dusseldorf, GE

12h50 – 14h00 : Déjeuner / Lunch

Visite de stands / Visit of stands

14h00 – 15h00 : Conférence invitée / Invited Talk

Development of a Network Topology Discovery Algorithm

Jean-Raymond Abrial, Consultant, Marseille, FR

15h30 – 16h05 : The Teaching of Data Structures: a Balanced Presentation of Skew Heaps

Marc Guyomard, ENSSAT, Université de Rennes, FR

16h05-16h20 : Pause / Break

16h20 – 17h00 : Ten Years Disseminating the B Method,

Thierry Lecomte, ClearSy, Aix-en-Provence, FR

Jean-Raymond Abrial, conference in Nantes on June 7, 2010

2010-04-30T10:16:00.000+02:00

Jean-Raymond Abrial is invited for the 2010 conference. The new book of J.R. Abrial will be available for the conference.

http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569

Prologue: faultless systems – yes we can!; Acknowledgements; 1. Introduction; 2. Controlling cars on a bridge; 3. A mechanical press controller; 4. A simple file transfer protocol; 5. The Event-B modeling notation and proof obligations rules; 6. Bounded re-transmission protocol; 7. Development of a concurrent program; 8. Development of electronic circuits; 9. Mathematical language; 10. Leader election on a ring-shaped network; 11. Synchronizing a tree-shaped network; 12. Routing algorithm for a mobile agent; 13. Leader election on a connected graph network; 14. Mathematical models for proof obligations; 15. Development of sequential programs; 16. A location access controller; 17. Train system; 18. Problems; Index.

Conférences grand public JS 2010

2010-04-03T15:48:00.000+02:00

L'un des objectifs des Journées Scientifiques de l'Université de Nantes est de diffuser la culture scientifique et technique.

Cette année, le thème de l'enfant et son éducation est à l'honneur.

Les conférences et la table ronde programmées sont gratuites et accessibles à tous.

Programme prévisionnel

15h00-15h45 : Conférence « Comment la connaissance vient aux bébés » par Roger LÉCUYER, Professeur émérite en psychologie de l'enfant, à l'Université Paris V, spécialiste des compétences périnatales

16h00-16h45 : Conférence « Stratégies familiales et politiques éducatives » par Agnès VAN ZANTEN, directrice de recherche au CNRS, à l'Observatoire Sociologique du Changement

17h00-18h00 : Table ronde sur le thème de l'enfant et son éducation avec Roger LÉCUYER, Agnès VAN ZANTEN, Jean-Christophe ROZÉ (Chef du service de médecine néonatale au CHU Nantes), Catherine CHOQUET (Adjointe au maire de Nantes en charge de la petite enfance, de la santé et des personnes handicapées) et Agnès FLORIN (Professeur en Psychologie de l'enfant et de l'éducation à l'Université de Nantes)

Death of Robin Milner

2010-03-30T10:26:00.001+02:00

"Robin Milner, FRS FRSE
Professor Emeritus of Computer Science
It is with great sadness that we note the death of Robin Milner.
Robin worked at the Computer Laboratory in Cambridge from 1995 onwards, serving as Head of the Laboratory 1996–1999. Before that, he worked at the University of Edinburgh 1973–1994, where he was founding Director of the Laboratory for Foundations of Computer Science (LFCS). He was awarded the Turing Award in 1991.
Robin played a leading role in the development of many areas of Computer Science, focussing especially on its mathematical foundations but always with a sharp eye on practice. His intellectual legacy includes:

machine-assisted proof construction with the LCF approach, underpinning the HOL and Isabelle/HOL provers;
the design and formal definition of programming languages, especially of Standard ML, including work on type safety, type inference and module systems;
models of concurrent computation, particularly with the CCS and Pi-Calculus process calculi and their theories of compositional reasoning; and
the bigraph model of mobile informatic processes with its applications to bioinformatics and pervasive computing.

These provide the basis and tools for a great deal of current research, by many people worldwide.
Always an inspirational teacher and colleague, and a warm-hearted man, he will be greatly missed."

Robin Milner visited Nantes on 2007 for a conference.

http://www.cl.cam.ac.uk/misc/obituaries/milner/

Invited Speaker 2010

2010-03-20T14:58:00.002+01:00

3rd International Conference
From Research to Teaching Formal Methods:
The B Method (TFM-B'10)
June 7, 2010,  Nantes, France

Pierre Castéran

http://www.labri.u-bordeaux.fr/perso/casteran/

Commandes latex pour B, Latex commands for B

2010-03-20T14:55:00.000+01:00

Nous donnons le code ASCII et en face la commande Latex

: \in
/: \notin
<: \subseteq
/<:
><
=> \implies
% \lambda
; \comp
\/ \cup
/\ \cap
& \land
or \lor
! \forall
# \exists
--> \fun
+-> \pfun
>--> \bij
<--> \rel
|-> \mapsto
|> \rres
<| \dres
||> \nrres
<|| \ndrres
>+-> \pbij
+->> \psurj
>+-> \pinj
-->> \surj
>--> \inj
== \defs
<-- \leftarrow
|| \parallel
/= \neq
<= \leq
{} \emptyset
* \times (produit cartésien, cartesian product)

B in Brazil

2010-03-01T15:35:00.002+01:00

Sacomã station in Sao Paulo is now equipped with the COPPILOT System
Since January 10 2010, the new Sacomã station (Line 2 - green) in Brazil
is open to the public since its inauguration by Governor Jose Serra in Sao Paulo..

Course on B

2010-02-11T09:16:00.000+01:00

http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/coursb/cassettesjra.html

BNF, Bibliothèque Nationale de France :
http://catalogue.bnf.fr/servlet/ObtenirUC?idNoeud=1.1&ID=38314325&Regroupement=3&Ordre=1&host=catalogue

3rd International Conference From Research to Teaching Formal Methods: The B Method (TFM-B'10)

2010-02-01T08:10:00.002+01:00

First Call for papers
3rd International Conference
From Research to Teaching Formal Methods:
The B Method (TFM-B'10)
June 7, 2010,  Nantes, France
http://www.lina.univ-nantes.fr/apcb
------------------------------------------------
Invited Speaker:
Pierre Castéran / On Coq and B /

LaBRI, U. Bordeaux
------------------------------------------------------

Overview: We anticipate a rich exchange of experiments

on research and teaching Formal Methods, in particular

the B method.
We would like to cover various works going from

the elaboration of courses till the teaching materials

and the evaluation of students and teachers 
themselves.

------------------------------------------------------

TOPICS: 
The topics of interest for TFM-B'2010 include but

are not limited to:
- Experiences with formal methods teaching using B
- Teaching materials for the B method
- Case studies and exercises featuring the B method
- The B method in the software engineering curriculum
- Use of the B method in disciplines other

than software engineering
- New advances in the B method and their incorporation

into the teaching 
curriculum
- Tool supports for software engineering with the B method
- Teaching tool-equipped formal methods
- Teaching environments for model-based formal methods
- Combining the B method with other approaches
- Comparative studies on teaching formal methods
 . . .

------------------------------------------------------------------------------------
Important Dates:
Paper submission deadline            March 13, 2010
Notification of acceptance/rejection April 16, 2010
Final version of accepted papers     May   8,  2010
Workshop in Nantes, France           June  7,  2010
Proceedings with ISBN

-------------------------------------------------------------------------------------
Workshop Chairs:  Christian ATTIOGBÉ,

Dominique MERY

Local Organization: COLOSS Team www.lina.univ-nantes.fr
LINA,  UMR CNRS 6241,  University of Nantes

Contact: bdays)@(univ-nantes.fr
http://www.lina.univ-nantes.fr/apcb

"A genius writes code an idiot can understand, while an idiot writes code the compiler can't understand. " (Anon )

2010-01-20T10:12:00.002+01:00

Investigation into the teaching of B worldwide

2010-01-20T10:03:00.001+01:00

Investigation into the teaching of B worldwide

The Questionaire

Where is B taught ?
We would like to update the investigation carried out over a year ago by Marie Laure Potet.
Please fill in the following questionaire and return it to us.

University: B is taught in the following departments, on the following courses,
in the following years:
[So we can store as triples (Department, Course, year)]
Department: (E.g. Computer Science)
Course: (E.g. BSc Computer Science)
Year: (E.g. 1st, 2nd)
Duration of Course in lecture hours (e.g. 20 hours)
Do you use a tool? (If so which one?):
How long do the students spend using the tool in the lecturers presence?: (E.g. 20 hours)
Is B used in assignments (outside normal teaching hours)?:
What is the relation between the teaching of B and the teaching of mathematics and logic for IT:
Under which discipline is B taught (e.g. software engineering, programming etc.):
Name of course contact:
Email address:
Type of assessment (e.g. supervised project, group project, machine-based exam):
Have you written course notes?:
Would you be prepared to share them with colleagues?:
-------------------------
The responses to this questionaire have been provided by:
Surname:
First Name:
Postal Address:
E-mail Address:
They are correct as of the date:
--------------------------
Please circulate to other interested parties.
H. Habrias.
We will send an analysis of the results of the questionaire to everyone who has filled one in.
The information provided will be available from one or several web sites. If you do not want your information to be made publicly
available then please do not provide it.
We abide by the freedom of information act.
Completed questionaires (and any questions) should be addressed to:
Henri Habrias
henri dot habrias at univ-nantes dot fr

The answers (2002 !)

http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/coursb/RepEnqueteFin06.html

Prof. Jean-Raymond Abrial : Managing the Construction of Large Computerized Systems

2010-01-12T12:19:00.003+01:00

http://www.inf.ethz.ch/news/focus/res_focus/feb_2005

Modeling in Event-B

2010-01-04T15:41:00.000+01:00

Modeling in Event-B
System and Software Design
Jean-Raymond Abrial
Swiss Federal University (ETH), Zürich
Hardback
(ISBN-13: 9780521895569)
Not yet published - available from June 2010
(Stock level updated: 12:41 GMT, 04 January 2010)
c. £60.00

http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569
http://www.event-b.org/abook.html

Software Specification Methods: An Overview Using a Case Study

2009-12-22T21:58:00.000+01:00

http://www.ebooks.com/ebooks/book_display.asp?IID=261397

1. Z – J. Bowen;
2. SAZ – F. Polack;
3. B – H. Diab and M. Frappier;
4. From UML Diagrams to B Specifications – R. Laleau and A. Mammar;
5. UML+Z: Augmenting UML with Z – N. Amalio, F. Polack and S. Stepney;
6. ASM – E. Börger, A. Gargantini and E. Riccobene;
7. TLA+ – L. Lamport; Part 2 - Event-Based Approaches
8. Action Systems – J. Sinclair;
9. Event B – D.Cansell and D. Méry
etc.

ABZ 2010

2009-12-22T21:52:00.000+01:00

ASM, Alloy, B and Z
Orford, Québec, Canada
February 22-25, 2010
http://abzconference.org/

Event-B and Rodin Documentation Wiki

2009-11-25T11:31:00.000+01:00

http://wiki.event-b.org/index.php/Main_Page

This is the documentation wiki for the Event-b.org site providing documentation for users and developers of the Rodin toolset.
Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.

métro de Sao Paulo, Sao Paulo Metro

2009-11-25T10:41:00.002+01:00

November 2009,
We are delighted to announce the signing of a contract
with the Sao Paulo underground system for the development,
delivery and installation of the SIL3 COPPILOT security system, responsible
for controlling the opening and closing of the screen doors, which will be
installed on lines 2 and 3 of the Sao Paulo Metro...

Novembre 2009,

Nous avons le plaisir de vous annoncer la signature d'un contrat avec le métro de Sao Paulo pour le développement, la livraison et
l'installation du système sécuritaire SIL3 COPPILOT, chargé de la commande d'ouverture et de fermeture des portes palières qui vont être
installées sur les lignes 2 et 3 du Métro de Sao Paulo...

Message de Clearsy

Supports de la journée B de novembre 2002 à Nantes

2009-11-24T13:02:00.000+01:00

http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/JourneeBNov02/JBSupports.html

Difference between Z and B

2009-11-24T12:59:00.000+01:00

http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/coursb/diffzetb.html

Lundi 7 juin 2010, prochaine conférence Teaching B

2009-11-24T11:26:00.002+01:00

Toujours à la Cité des Congrès de Nantes.

Recent Innovations and Applications in B

2009-09-25T21:03:00.000+02:00

http://www.bmethod.com/php/conference-workshop-recent-innovations-and-applications-in-B-en.php

Rodin workshop

2009-08-02T19:05:00.001+02:00

The Rodin workshop took place last week and
abstracts and slides are available on the Event-B wiki:

http://wiki.event-b.org/index.php/Rodin_Workshop_2009

A follow-on workshop will be held next summer.
Date and venue to be decided.

Michael Butler



On 21/05/2009 15:39, "Michael J Butler"
 <mjb@ecs.soton.ac.uk> wrote:

A reminder about the Rodin Developer Workshop
in Southampton in July 2009:

http://www.event-b.org/rodin09.html

Note that we have now decided to hold
 a 1-day tutorial on Rodin plug-in
development on 15 July just before
the workshop. The tutorial is intended
for existing and prospective plug-in
developers. It will give an overview
 of the architecture of Rodin and
 provide guidance on building plug-ins.

ORGANISERS:

Michael Butler, University of Southampton
Stefan Hallerstede, Heinrich-Heine-Universität Düsseldorf
Laurent Voisin, Systerel

Formal Methods Week

2009-08-02T14:51:00.000+02:00

http://www.win.tue.nl/fmweek/

conference workshop: recent innovations and applications in B

2009-08-02T14:48:00.000+02:00

http://www.bmethod.com/php/conference-workshop-recent-innovations-and-applications-in-B-en.php

Conférence grand public : le réchauffement climatique

2009-06-09T08:05:00.008+02:00

Vincent Courtillot, J.M. Salles, J. Girardeau et le présentateur.
Le discours opposé à celui de Vincent Courtillot se trouve par exemple ici
Une pétition citée par V. Courtillot est ici

Conference : programme

2009-06-09T07:47:00.001+02:00

8:30-9:00 Welcome

9:00-10:00 Invited Conference

Prof. Michael Leuschel, University of Düsseldorf details

10:00-10:15 Break

10:15-11:00 Latest News on AtelierB V4

Antoine Requet, ClearSy, France details

11:00-11:35 Sculpturing Event-B Models with Rodin: Holes and Lumps in Teaching Refinement through Problem-Based Learning

J. Paul Gibson, Eric Lallet, Jean-Luc Raffy, Telecom& Management SudParis, France

11:35-11:50 Break

11:50-12:25 Teaching the B Method at Oxford Brookes

D. Lightfoot, C. Martin, Oxford Brookes University, UK

12:25-13:00 Twelve Years of B Teaching in an Engineer School : from a Correct by Design Approach to Analysis Techniques and Tools

M-L. Pottet, Verimag Grenoble, France

13:00-14:00 Lunch

14:00-14:35 High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin

Mireille Samia, Harald Wiegard, Jens Bendisposto, Michael Leuschel, University of Düsseldorf, DE

14:35-15:10 BiCoax, a Proof Tool Traceable to the BBook

Samuel Colin, George Mariano, INRETS, France

15:10-16:15 Break - Demos

16:15-16:50 Constructing a Formal Event Model of Linux File System Access Permissions: A Research-Based Teaching Approach

David Cumbor, Bill Stoddard, University of Teesside, UK

16:50-17:25 How to make mistakes?

Stefan Hallerstede, University of Düsseldorf, DE

17:25-18:00 To structure, Realize and Prove: How and Why

Alain Couturier(1), Michel Gazeau(1), Gérald Jean-Baptiste(1), Gwenola Kerglonou(2), (1) CNAM Pays-Loire and (2) ICAM Nantes, France

Conference June 8-2009

2009-06-09T07:30:00.008+02:00

The invited conference of Prof. Michael Leuschel, University of Düsseldorf, and the conference of J. Paul Gibson.
The public of the conference.

During your stay in Nantes, go and see the wolfs in the castle of Nantes

2009-06-07T14:26:00.005+02:00

Royal de Luxe. The giants are in the city ! Programme

2009-06-05T13:17:00.004+02:00

More pictures HERE

Vendredi 5 juin : La petite géante devrait se réveiller vers 11h place Viarme et le scaphandrier géant devrait émerger du bassin Saint-Félix vers 13h30 au niveau du pont Tbilissi. Ils parcourront ensuite les rues de Nantes le vendredi après-midi (chacun de leur côté ou ensemble ?) : le scaphandrier devrait atteindre la place de la petite Hollande vers 15h avant de se reposer. Le spectacle reprendra ensuite vers 19h.

Samedi 6 juin : Un réveil est prévu samedi 6 juin à partir de 10 h au niveau du château (à proximité des loups en liberté dans les douves).

Dimanche 7 juin : Ils embarqueront à bord d’un chaland vers 11h à proximité du pont Anne de Bretagne (et donc du grand éléphant :-). Le bel équipage naviguera en direction de Saint-Nazaire via Indre, Couëron, Le Pellerin, Frossay et Paimboeuf. L’arrivée à St-Nazaire est prévue vers 17 h et la fin du spectacle, en début de soirée vers 20h/20h30.

Photos taken this morning (5-06-2009, 11h 30)

Royal de Luxe, Where, When, What ?

2009-06-02T09:30:00.001+02:00

HERE

All is free.

Nantes

2009-05-20T21:20:00.005+02:00

From the Airport/Train Station to the Cité des Congrès

2009-05-18T17:46:00.001+02:00

The Cité des Congrès is very close to the Railway Station (Gare TGV, sortie Sud) (don't use a taxi or a public transportation). The Gare TGV sortie Sud is also the stop of the airport shuttle (navette aéroport TAN).

The City of Congress brings you the Cité pass ( City Pass) allowing access to the entire public transportation network of Nantes ( TAN) , including airport shuttles. The Cité Pass is valid only on Monday, June 16, 2008. If you wish to receive the Cité Pass please ask us before your arrival at Nantes.

From the airport Nantes Atlantique to Nantes

2009-05-18T17:44:00.000+02:00

You can use (with the cité pass). Ask your FREE Cité pass to use the public transportations :

the airport shuttle (tanair), Bus, 19 minutes
a bus connected to the tramway (tan) :

- Bus n° 37, Direction Croix Jeannette, Arrêt (stop) Neustrie

- then Tram 3, direction Sillon de Bretagne, Arrêt (stop) Commerce. Here you will find a lot of buses and tramways

"Data Semantics"

2009-05-12T14:58:00.003+02:00

Two pages of Data Semantics, J.R. Abrial, IFIP WC on Data Base Management, Cargèse, Corsica, France, 1-5 April 1974,
Proceedings edited by J.W. Klimbie and K.L. Koffeman, North-Holland

Specification or how yo make Abstraction Real

2009-05-12T11:27:00.005+02:00

Click on the image to enlarge it.

TSI, vol. 3, n° 3, 1984
The two first pages. To read the entire paper go here

Yes, you are in Nantes !

2009-05-12T09:36:00.004+02:00

Ile de Versailles (Japon) et Parc du Grand Blottereau (Corée)

Registration

2009-05-11T13:56:00.001+02:00

http://www.lina.sciences.univ-nantes.fr/apcb/BDayNantes2009/registration.html

During the Journées Scientifiques 2009

2009-05-09T15:53:00.001+02:00

2 conférences grand public :

"Le réchauffement climatique" par Vincent COURTILLOT ;

"Peut-on donner une valeur marchande à la biodiversité ?" par Jean-Michel SALLES,

Bienvenue à Nantes, la ville où le monde se retrouve !

2009-05-09T15:29:00.005+02:00

Royal de Luxe, Nantes. June 7-2009, Do not miss Royal de luxe !

Enjoy the B Conference to follow the free show by Royal de luxe!

Welkom in Nantes!

ナントへようこそ

Bine ati venit la Nantes !
Benvenuti a Nantes
Καλώς ήρθατε στην Ναντ !
Bem-Venido a Nantes
Failte go Nantes
Welcome to Nantes
Welkommen til Nantes
Willkommen in Nantes
مرحبا بكم في نانت

Добро пожаловать в Нанте!

Read the archives 2008

2009-05-08T21:44:00.002+02:00

you will find information on transportation, hostels, etc.
HERE

Le Trois-Mâts Belem à Nantes

2009-05-08T21:39:00.002+02:00

Le Trois-Mâts, construit et lancé à Nantes en 1896, se visite les 6 et 7 juin 2009. Il est l’un des plus anciens grands voiliers naviguant au monde.
France's only remaining three masted barque, one of the oldest tall ships still sailing the seas...

Photos

The web site
http://www.fondationbelem.com/the_official_website_of_the_three-masted_ship_belem.htm

The B method : from Research to Teaching

B et cryptographie

FM 2012

原书名： The B-Book:Assigning Programs to Meanings

基本信息

Techniques industrielles de modélisation formelle pour le transport

Fourth NASA Formal Methods Symposium

Tutorial on the Event-Based B Method

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

Composys

ABZ 2012

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

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

Une Deuxième Révolution Galiléenne

Les Journées Scientifiques 2011 de l'Université de Nantes

WWV 2011 Automated Specification and Verification of Web Systems

Workshop B 2011, colocated with FM 2011, Limerick, Ireland, june, 21, 2011

the release of ProB for Rodin 2.1

Have we learned from the Wasa disaster ? J.R. Abrial

http://videotorium.hu/en/recordings/details/1674,Have_we_learned_from_the_Wasa_disaster_

FM 2011: 17TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

Structures de données et méthodes formelles, Marc Guyomard, Springer

Décès de Michel Sintzoff

http://www.ae-info.org/ae/User/Sintzoff_Michel

FSEN '11

The Space and Motion of Communicating Agents

Cours et exercices corrigés d'algorithmique

Death of Jean-Claude Laprie

Méthodes de spécification de systèmes temps réel en B

THE PROGRAMMING LANGUAGE B

B vs. Coq to prove a Garbage Collector

Processus de validation basée sur la notion de propriété

Formal Methods in Safety-Critical Railway Systems

Vers une méthodologie de Validation et de Vérification multi-formelle des Interfaces Utilisateurs en milieu industriel

The Development of a Probabilistic B-Method and a Supporting Toolkit

Les bases du langage B

A formal specification of the javaByte code semantics using the B method

Using B Method to Formalize the Java Card Runtime Security Policy for a Common Criteria Evaluation

How to formally specify the Java Bytecode semantics using the B method

Formalisation and Veri¯cation of the GlobalPlatform Card Speci¯cation Using the B Method

ProB: An Automated Analysis Toolset for the B Method

Applying the B Formal Method to the Bossa Domain-Specific Language

Cooperation Between the B Method and the Automata Theory to Check the Component Interoperability

PBS, support of the B Method in PVS, Cesar Munoz, SRI

Component-based Development using the B method

Tutorial on the B method

The B Method for Programmers

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

Program Development by Refinement: Case Studies Using the B Method (Formal Approaches to Computing and Information Technology (FACIT))

Security of Computer Architectures, Jean-Louis Boulanger

Le dernier livre d'Umberto Eco en français

Dall'albero al labirinto. Studi storici sul segno e l'interpretazione

Studi storici sul segno e l’interpretazione

http://bompiani.rcslibri.corriere.it/libro/5902_dall_albero_al_labirinto_studi_eco.html

FM 2011 (20-24 June 2011, Limerick, Ireland): Call for Tutorials

Workshop on B Dissemination

B方法 , The B Book in chinese

基本信息

综合

计算机

软件工程

General-Service Ballistic Computer Programming Based on B-Method

Formal development of a washing machine controller by using formal design patterns

Event Model Decomposition

The papers and the slides of the conference 2010 are here ...

L'Université de Nantes a 550 ans cette année

On line registration for the 2010 Conference

Programme of the 2010 conference

Jean-Raymond Abrial, conference in Nantes on June 7, 2010

Contents

Conférences grand public JS 2010

Programme prévisionnel

Death of Robin Milner

Invited Speaker 2010

Commandes latex pour B, Latex commands for B

B in Brazil

Course on B