Thursday, March 22, 2012

B 2012 - a FM2012 satellite workshop

**********************************************************************
                        DEADLINE EXTENSION

          Abstract submission: March 23, 2012
          Full paper submission: April 2, 2012

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


                         B 2012 - a FM2012 satellite workshop
                            Paris, France, August 28, 2012


http://membres-liglab.imag.fr/idani/B2012


OBJECTIVES

The B2012 workshop, co-located with FM, provides an opportunity to
widely gather the B community (from academia, industry and
administration). The idea is to cover an ample spectrum of topics, from
theoretical advances, tool support, industrial practice, new application
domains as well educational practice. It is also the place to hear about
recent advances in current industrial applications using B. Papers
discussing new ideas that are at an early stage of development are also
welcome.


INDICATIVE LIST OF TOPICS

Main topics addressed by the workshop are many, including but not
limited to:

• Theoretical advances : refinement, composition, code generation,
verification and proofs
• Modeling challenges, guidelines for formal development, integration of
B in software and
systems engineering
• Tool development, tool usage reports
• Case studies, return of experience, methodology, scaling up
• Teaching and training
• New perspectives

PAPER SUBMISSION

We invite two kinds of papers: long and short papers. Accepted long
papers will be published in ENTCS following the workshop.

• Long papers (10 ENTCS pages) dedicated to presenting research findings
in the identified topic areas of the workhop. Papers must describe
original work that does not substantially overlap with papers that have
been published or that are simultaneously submitted to a journal,
conference, or workshop with refereed proceedings.

• Short papers (max 6 ENTCS pages) dedicated to work in progress,
teaching experiments or case study. They do not constitute a refereed
publication. Hence, this will avoid any constraints on later publication.

Papers must follow the ENTCS guidelines
(http://www.entcs.org/prelim.html) and be submitted in PDF format and
will be handled via EasyChair
(https://www.easychair.org/conferences/?conf=b2012).


PROGRAM COMMITTEE :


Marie-Laure Potet -Vérimag – University of Grenoble – France (Chair)
Stefan Hallerstede - Aarhus University, Denmark(Co-chair)

Yamine Aït-Ameur, IRIT-ENSEEIHT, Toulouse, France
Christian Attiogbé, University of Nantes, France
Richard Banach, University of Manchester, IK
Michael Butler, university of Southampton, UK
Mamoun Filali, CNRS, University of Toulouse, France
Marc Frappier, Université de Sherbrooke, Québec, Canada
Stefan Hallerstede - Aarhus University, Danmark
Andrew Ireland, Heriot-Watt University, UK
Jacques Julliand, LIFC, University of Besançon, France
Régine Laleau, University of Paris-Est, France
Thierry Lecomte, Clearsy, France
Michael Leuschel, University of Düsseldorf, Germany
Anamaria Martins Moreira, UFRN, Natal, Brazil
Marie-Laure Potet, VERIMAG, University of Grenoble, France
Emil Sekerinski, McMaster University, Canada
Helen Treharne, University of Surrey, UK
Laurent Voisin, Systerel, France
Marina Waldén, Åbo Akademi University, Turku, Finland







-- 
Marie-Laure Potet
Prof. Grenoble INP

VERIMAG - Centre Equation
2 avenue de Vignate
38610 GIERES
FRANCE

Mail: Marie-Laure.Potet@imag.fr
Tel: +33 (0) 4 56 52 04 28
Fax:  +33 (0) 4 56 52 03 44

http://www-verimag.imag.fr/~potet

To reach us:
http://www-verimag.imag.fr/index.php?page=plan


History : Z in U.K. with A. Hoare

" Bowen: This led up to your CSP book in your own red and white book series in 1985, but you were also
working on other things. You were very much promoting a new formal notation that became known as Z
at Oxford, although maybe you weren’t directly working on it. I understand you were involved in inviting
Jean-Raymond Abrial for instance, who very much promoted Z and defined Z. Would you like to say
something about how that started?

Hoare: Yes, it’d be a pleasure. I met Jean-Raymond Abrial at a summer school organized by Electricite
de France in a lovely little village in France called Labrae sonnalp [sp]. I was very impressed by his
research, and indeed his lecturing. He was a brilliant lecturer. I invited him to spend some research time
at Oxford, and got a research grant for him from the Research Council. He did marvelous work in the
development of Z. This is a sort of specialization of the techniques of logic and set theory, which were
originally thought of as the foundation of mathematics in the earlier part of the last century, and now being
suggested as a suitable notation and conceptual framework for specifying the desired properties of
computer systems. The formal theory was adapted for this purpose and tried out in a number of small
and other realistic and large sized examples, and found to be surprisingly effective at describing what a
program is intended to do, rather than how the program works, how the program actually does it.
Bowen: I think you were involved with encouraging IBM to actually take up the ideas. How did that
come about?

Hoare: Again, it was very much a matter of chance. I was invited to give a keynote address at the British
Computer Society Symposium on professionalism, I think it was, in programming. I talked a bit about
formalization and verification, and put forward a conjecture, fairly tentatively, that maybe the time was
right to scale these things up by trial use in industry. In the audience there happened to be quite a senior
director from IBM at Hursley. He came up to me after the lecture, and invited me to put my commitment
where my mouth was, and actually do something in collaboration with IBM. That made me gulp a bit,
because I knew that -- well, I had the impression -- that IBM had produced some pretty complicated
software, and this really would be a challenge, and there was a good chance that we would fall flat on our
faces. But you can’t turn down an opportunity like that. So Abrial and Ib Sorensen and other colleagues
set to work, and actually produced some very useful analyses for them, using Z, to help them with anongoing project for restructuring and rewriting parts of their software system, a software system called
CICS, C-I-C-S. It stands for Customer Information Control System. It was one of the most profitable and
influential software products in those days, so it was an important project.

Bowen: That led to a Queen’s award for technology. [...]

source :
J.P. Bowen
Oral History of Sir Antony Hoare
CHM Ref: X3698.2007 © 2006 Computer History Museum Page 18 of 25