********************************************************************** 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
Thursday, March 22, 2012
B 2012 - a FM2012 satellite workshop
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
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
Subscribe to:
Posts (Atom)
