Friday, October 4, 2013
4th International ABZ 2014 Conference ASM, Alloy, B, TLA, VDM, Z June 2 - 6 2014 Toulouse - France
http://www.irit.fr/ABZ2014/index.html
Important dates
| Research paper and answers to case study submission: | January 14, 2014 |
| Workshop proposal submissions: | October 15, 2013 |
| Short paper submission: | February 3, 2014 |
| Tutorial proposal submissions: | January 30, 2014 |
| Papers/abstract/answers to case study notification: | March 1, 2014 |
| Workshop proposal notifications: | November 30, 2013 |
| Final Version due: | March 20, 2014 |
| Tutorial proposal notifications: | Febuary 28, 2014 |
| Main ABZ 2012 conference: |
Tuesday, September 17, 2013
Thursday, August 29, 2013
2015 FM symposium
Formal Methods Europe is inviting proposals for the 2015 FM symposium
http://fmeurope.hosting.west.nl/mailman/listinfo/events
Sunday, April 7, 2013
FME Workshop on Formal Methods in Software Engineering held in conjunction with ICSE 2013
CALL FOR PARTICIPATION: FormaliSE 2013 FME Workshop on Formal Methods in Software Engineering held in conjunction with ICSE 2013 Saturday 25 May 2013, San Francisco, USA http://www.formalise.org/ WORKSHOP SCOPE The software industry has a long-standing and well-earned reputation for failing to deliver on its promises and it is clear that still nowadays, the success of software projects with the current technologies cannot be assured. For large complex projects ad hoc approaches have proven inadequate to assure the correct behavior of the delivered software. The lack of formalization in key places makes software engineering overly sensitive to the weaknesses that are inevitable in the complex activities behind software creation. Aids to precision in each phase of software development and crosschecking are essential, and this is precisely one the objectives of formal methods. After decades of research, and despite significant advancement, formal methods are still not widely used in industrial software development. This may be due to the fact that the formal methods community has not enough focused its attention to software engineering needs, and its specific role in the software process. At the same time, from a software engineering perspective, there could be a number of fundamental principles that might help to guide the design of formal methods in order to make them more easily applicable in the development of software applications. The main goal of the workshop is to foster integration between the formal methods and the software engineering communities with the purpose to examine the link between the two more carefully than is currently the case. PROGRAM Invited keynote: Though this be madness, yet there is method in it? Alan Wassyng (McMaster University, Canada) Session 1: Specification Do You Speak Z? Formal Methods under the Perspective of a Cross-Cultural Adaptation Problem Andreas Bollin (Alpen-Adria Universitat, Austria) Session 2: Verification Functional SMT solving with Z3 and Racket Siddharth Agarwal and Amey Karkare (Indian Institute of Technology Kanpur, India) Trace Based Reachability Verification for Statecharts Kumar Madhukar, Ravindra Metta, Ulka Shrotri and R. Venkatesh (Tata Consultancy Services, India) An Integrated Data Model Verifier with Property Templates Jaideep Nijjar, Ivan Bocic and Tevfik Bultan (University of California at Santa Barbera, USA) Session 3: Application of Formal Methods Towards a Formalism-Based Toolkit for Automotive Applications Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson and Manuel Mazzara Recommendations for Improving the Usability of Formal Methods for Product Lines Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih and Pourya Shaker (University of Waterloo, Canada) Lightweight Formal Models of Software Weaknesses Robin Gandhi, Harvey Siy and Yan Wu (University of Nebraska at Omaha, USA) Session 4: Timed systems Automatic Validation of Infinite Real-Time Systems Thomas Göthel and Sabine Glesner (Technische Universitat Berlin, Germany) A framework for the rigorous design of highly adaptive timed systems Louis-Marie Traonouez, Axel Legay, Maxime Cordy and Pierre-Yves Schobbens (University of Namur, Belgium, and INRIA Rennes, France) Closing: Round table and discussion For more details see www.formalise.org, REGISTRATION for the workshop is open, see http://2013.icse-conferences.org/content/registration (early registration with reduced rates closes on 14 April 2013). For HOTELS and VENUE see http://2013.icse-conferences.org/content/venue OC/PC CHAIRS Stefania Gnesi (ISTI-CNR, Italy) Nico Plat (West Consulting BV, The Netherlands). The OC/PC Chairs can be reached via e-mail: oc@formalise.org. PROGRAM COMMITTEE * Yamine Ait-Ameur (IRIT/ENSEEIHT, France) * Manfred Broy (Technical University München, Germany) * Jürgen Dingel (Queen's University, Canada) * Cindy Eisner (IBM Haifa Research Laboratory, Israel) * Arie Gurfinkel (Carnegie Mellon University, USA) * Patrick Heymans (University of Namur, Belgium, and INRIA, France) * Alessandro Fantechi (Università di Firenze, Italy) * Connie Heitmeyer (Naval Research Laboratory, USA) * Mike Hinchey (Lero, Ireland) * Axel van Lamsweerde (University of Louvain. Belgium) * Peter Gorm Larsen (Aarhus University, Denmark) * Marc Lawford (MacMaster University, Canada) * Thierry Lecomte (ClearSy, France) * Yves Ledru (IMAG, France) * Antónia Lopes (University of Lisbon, Portugal) * Tiziana Margaria (Potsdam University, Germany) * Henry Muccini (Università dell’Aquila, Italy) * Isabelle Perseil (Inserm, France) * Steve Riddle (University of Newcastle, UK) * Matteo Rossi (Politecnico di Milano, Italy) * Wolfram Schulte (Microsoft, USA) * Elena Troubitsyna (Abo University, Finland) * Sebastián Uchitel (Imperial College and Universidad de Buenos Aires) * Willem Visser (University of Stellenbosch, South Africa) * Fatiha Zaïdi (LRI/CNRS, France) _______________________________________________ events mailing list events@fmeurope.org http://fmeurope.hosting.west.nl/mailman/listinfo/events
Inscription aux Journées Scientifiques de l'Université de Nantes, 2013
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
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
Monday, January 30, 2012
FM 2012
CALL FOR PAPERS FM 2012
*********************************************
18TH INTERNATIONAL SYMPOSIUMON 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
Subscribe to:
Posts (Atom)
