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

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

Contents

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

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

"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

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

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

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

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)

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 )

Investigation into the teaching of B worldwide

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