Saturday, December 14, 2013

how to do a design starting from a model that is gradually refined toward executable code


http://www.youtube.com/watch?v=fSWZWXx5ixc
In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.


http://www.youtube.com/watch?v=p6D0RSo3TAY
Using an extended example that flattens and reconstructs trees, Sophia Drossopoulou and Rustan Leino show how to write inductive proofs of functional programs. The verification tool checks the correctness of the proofs. Proofs can be given in full detail, as they might be when a person first writes the proof or when the proof is intended for human understanding. Alternatively, proofs can be written with less detail, akin to the way a confident mathematician elides some details. In either case, the verification tool is satisfied only if it can fill in the missing pieces of the proof.

http://www.youtube.com/watch?v=xg4wZDJuk6o

In this episode, Kuat Yessenov and Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, show how a program can be constructed by stepwise refinement.

http://www.youtube.com/watch?v=P2durYFsJSA
Jason Koenig and Rustan Leino show a verification problem that makes use of functions, ghost variables, and lemmas.

http://www.youtube.com/watch?v=BLQo5d3hI4M
In this episode, Rosemary Monahan and Rustan Leino use problems specified using comprehension expressions to demonstrate how a problem can be solved using partial solutions

http://www.youtube.com/watch?v=kbJO-U9Wp-s

In this episode, Rustan Leino shows how to prove loop termination. During his demonstration, Rustan presents the theoretical background information necessary to build the proof before modeling it using the Dafny language.


In this episode, Rustan Leino talks about loop invariants. He gives a brief summary of the theoretical foundations and shows (using a problem to compute cubes) how a program can sometimes be systematically constructed from its specifications.

K. Rustan M. Leino

The Verification Corner is a video series on YouTube that explains different concepts of software verification.

Atelier B

http://www.atelierb.eu/

Conférence de J.R. Abrial à l'Université de Sherbrooke

http://www.usherbrooke.ca/carrefour/archives/archives-des-conferences/2008/mais-si-on-peut-developper-des-systemes-informatiques-sans-fautes/

Conférence de Jean-Raymond Abrial, docteur d'honneur en sciences 2008 à l'UdeS
12 septembre 2008
Professeur invité à l'École polytechnique fédérale de Zurich en Suisse depuis 2004, Jean-Raymond Abrial présente une conférence publique qui s'intitule « Mais si, on peut développer des systèmes informatiques sans fautes! ». Cette présentation se veut en lien direct avec ses grands projets de recherche dans lesquels il s'est investi tout au long de sa carrière exceptionnelle. À l'Agora du Carrefour de l'information, le vendredi 12 septembre 2008, à midi. Jean-Raymond Abrial est venu à Sherbrooke recevoir le 13 septembre le tout premier doctorat honoris causa en sciences dans le domaine de l'informatique de l'Université de Sherbrooke.

Papers of J.R. Abrial

http://www.informatik.uni-trier.de/~ley/pers/hd/a/Abrial:Jean=Raymond

Formalizing Hybrid Systems with Event-B

Abstract State Machines, Alloy, B, VDM, and ZLecture Notes in Computer Science Volume 7316, 2012, pp 178-193Formalizing Hybrid Systems with Event-B

Abstract

From Z to B and then Event-B: Assigning Proofs to Meaningful Programs

Integrated Formal MethodsLecture Notes in Computer Science Volume 7940, 2013, pp 1-15From Z to B and then Event-B: Assigning Proofs to Meaningful Programs
Abstract

Set-Theoretic Models of Computations

Theories of Programming and Formal MethodsLecture Notes in Computer Science Volume 8051, 2013, pp 1-22Set-Theoretic Models of Computations

Abstract

Event-B patterns and their tool support

Software & Systems ModelingVolume 12Issue 2pp 229-244Event-B patterns and their tool support

FormaliSE 2014 2nd FME Workshop on Formal Methods in Software Engineering



Call for Papers: FormaliSE 2014
2nd FME Workshop on Formal Methods in Software Engineering
held in conjunction with ICSE 2014 (May 31th–June 7th)
Hyderabad, India
NTRODUCTION

IThe 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
ey places makes software engineering overly sensitive to the weaknesses that
the correct behavior of the delivered software. The lack of formalization in
k are inevitable in the complex activities behind software creation. Aids to precision in each phase of software development and crosschecking are
n in
both thinking and documenting the preliminary stage of the softwa
essential, and this is precisely one the objectives of formal methods. Formal methods (FMs) are intended to provide the means for greater precisi
ore creation process. When done well, this can aid all aspects of software creation: user requirement formulation, implementation, verification/testing, and the creation
ed by practitioners, and the integration of such tools with
activities that
of documentation. However, the maturing of formal techniques into real-life software engineering involves providing notations and tools that are readily understood and u
s are far from the unrealistic assumptions that characterized some earlier research in formal methods. After decades of research, and despite significant advancement, formal methods
needs, and its specific role in the software
process. At the same time, from
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 engineerin
g 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.
EST include but are not limited to:
- integration of FMs in the software
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. AREAS OF INTE
Rdevelopment life cycle - ability of formal methods to handle real-world problems - prescriptive/objective guidance in the use of FMs - Formal methods in a certification context - “lightweight” or usable FMs - application experiences - scalability of FM applications - experimental validation
e Proceedings Format. They
will be published as part of the (electronic) pro
The program will start with an invited speaker, followed by presentations of submitted papers. The workshop will end with a round table discussion (PC members and workshop audience), focusing on the subjects that came up during the workshop. SUBMISSIONS are limited to 7 pages in IEEE Conferen
cceedings of ICSE 2013. All papers submitted to the workshop must be unpublished original work and should not be under review or submitted elsewhere while being under consideration. All submissions must be in English and in PDF format through online upload to the workshop submission website at the following URL:
members will review all submissions. Papers will be judged on the basis of
their clarity, relevance, originality, and contribution to the field.
s
24 February 2
IMPORTANT DATES 24 January 2014: submission deadline for workshop pape
r014: notification of acceptance/rejection to authors
papers
*** Exact date *** 2014: FormaliSE workshop held in H
14 March 2014: camera-ready copy deadline for worksho
pyderabad, India OC/PC CHAIRS are Stefania Gnesi (ISTI-CNR, Italy) and Nico Plat (West
vices, India). The OC/PC Chairs can be reached via e-mail:
Consulting BV, The Netherlands). Local organizer is Ravindra Metta (Tata Consultancy Se
roc@formalise.org. If you intend to submit a paper you are invited to inform us
in advance.
OMMITTEE consists of Andreas Bollin (Klagenfurt University,
Austria), Ei
THE PROGRAM
Cnar Broch Johnsen (Oslo University, Norway), Manfred Broy
rk University, UK),
Nancy Day (University of Waterloo, Canada), Cindy Eisner (
(Technical University München, Germany), Ana Cavalcanti (Y
oIBM Haifa Research Laboratory, Israel) , Alessandro Fantechi (University of Florence, Italy), Jaco
echnology, The Netherlands), Arie Gurfinkel (Carnegie
Mellon University,
Geldenhuys (University of Stellenbosch, South Africa) , Jan Friso Groote (Eindhoven University of
TUSA), Mike Hinchey (Lero, Ireland), Randolph Johnson (independent consultant, USA), Axel van Lamsweerde (University of Louvain.
France), Yves Ledru
(IMAG, France), Axel Legay (INRIA Rennes, France),
Belgium), Peter Gorm Larsen (Aarhus University, Denmark), Marc Lawford (MacMaster University, Canada), Thierry Lecomte (ClearSy,
Antónia Lopes (University of Lisbon, Portugal), István Majzik (Budapest University of Technology and Economics, Hungary), Tiziana Margaria (Potsdam University, Germany), Ravindra
Finland) , Sebastián Uchitel (Imperial College and
Universidad de Buenos Aires,
Metta (Tata Consultancy Services, India), Henry Muccini (Universita degli Studi dell’Aquila, Italy), Matteo Rossi (Politecnico di Milano, Italy), Elena Troubitsyna (Abo University,
UK and Argentina), Hironori Washizaki (Waseda
France).
University, Japan), and Fatiha Zaïdi (LRI/CNRS,


Monday, November 11, 2013

EB2ALL - The Event-B To C, C++, Java And C# Code Generator

http://eb2all.loria.fr/

"EB2ALL is a set of translator tools that automatically generates efficient target programming language code (C, C++, Java and C#) from Event-B formal specification related to the analysis of the complex problems. The EB2ALL contains four plugin namely EB2C, EB2C++, EB2J and EBC#. The goal of EB2ALL is to be able to generate a verified source code that satisfies behavioral properties of the develop formal system (abstractly). The EB2ALL tool is developed as a set of plugins for RODIN development tool under the Eclipse framework. RODIN is an integrated development environment (IDE) for developing Event-B models. The RODIN tool is written entirely in Java and build on top of the Eclipse platform."

Courses

http://www.loria.fr/~mery/erasmusmaynooth/

Tuesday, November 5, 2013

First International Workshop on Formal Integrated Development Environments (Satellite event of ETAPS)

Call for Papers - F-IDE 2014 - April 6th, 2014, Grenoble, France

Call for Papers
First International Workshop on Formal Integrated Development Environments
(Satellite event of ETAPS)
April 6th, 2014, Grenoble, France
http://www.ensta-paristech.fr/~etaps/

WORKSHOP AIM

High levels of safety, security and also privacy standards require the
use of formal methods to specify and develop compliant software
(sub)systems.  Any standard comes with an assessment process, which
requires a complete documentation of the application in order to ease
the justification of design choices, code review and proofs. Ideally,
an F-IDE dedicated to such developments  should comply with several
requirements. The first one is to associate a logical theory with a
programming language, in a way that facilitates the tightly coupled
handling  of specification properties and program constructs. The
second one is to offer a language/environment simple enough to be
usable by most developers, even if they are not fully acquainted with
higher-order logics or set theory, in particular by making development
of proofs as easy as possible and as readable  as possible. The third
one is to offer automated management of application documentation. It
may also  be expected that developments done with such an F-IDE are
reusable  and modular.  Moreover, tools for testing andstatic analysis
may be embedded in this F-IDE, to address most steps of the assessment
process.

TOPICS

We encourage submissions presenting and discussing research efforts as
well as experience feedbacks on design, development, use of tools
aiming at making formal methods "easier" for non-specialists.  In this
context, the topics include (but are not limited to):

- F-IDE building : design and integration of languages, compilation

- How to make high-level logical and programming concepts palatable to
industrial developers

- Integration of Object-Oriented and modularity features

- Integration of static analyzers

- Integration of automatic proof tools, theorem provers and testing tools

- Documentation tools

- Impact of tools on certification

- Experience reports of developing F-IDE

- Experience reports of using F-IDE

- Experience reports of formal methods-based assessments of industrial
applications

We encourage not only mature research results but also submissions
presenting innovative ideas and early results are also of interest.

SUBMISSIONS

Papers  (6-14 pages in length), following EPCTS format are expected.
They can be:
- Research papers providing new concepts and results
- Position papers and research perspectives
- Experience reports
- Tool presentations

Submissions will be done via Easychair:
https://www.easychair.org/conferences/?conf=fide2014


PROCEEDINGS

Final versions of accepted papers will be published in a volume of the
Electronic Proceedings in Theoretical Computer Science (EPTCS).

IMPORTANT DATES

- Abstract submission : 18 December, 2013
- Paper Submission : 23 December, 2013
- Notification : 27 January, 2014
- Final version  : 10 February, 2014
- Workshop date:  April 6, 2014


PC CO-CHAIRS

- Catherine Dubois, Cédric / ENSIIE,  (dot)  (at) 
ensiie (dot) fr
- Dimitra Giannakopoulou, NASA Ames,  (dot)  (at) 
nasa (dot) gov
- Dominique Mery, LORIA / Université de Lorraine,  (dot)
 (at) loria (dot) fr

11th International Colloquium on Theoretical Aspects of Computing 17-20 September 2014, Bucharest, Romania

             CALL FOR PAPERS -- ICTAC 2014

**********************************************************************
   11th International Colloquium on Theoretical Aspects of Computing
               17-20 September 2014, Bucharest, Romania
                    http://fmi.unibuc.ro/ictac2014
**********************************************************************

ICTAC 2014 is the 11th International Colloquium on Theoretical Aspects 
of Computing and will bring together practitioners and researchers from 
academia, industry and government to present research and to exchange 
ideas and experience addressing challenges in both theoretical aspects 
of computing and in the exploitation of theory through methods and tools 
for system development. Another aim of ICTAC is to bring together 
researchers working on theoretical aspects of computing in order to 
present their recent results and to discuss new ideas concerning 
computer science.

THEMES AND TOPICS OF PAPERS

ICTAC 2014 calls for regular research papers on theories of computation 
and programming, foundations of software engineering and on formal 
techniques in software design and verification, as well as papers about 
tools that support formal techniques for software modeling, system 
design and verification.
The topical areas of the conference include, but not limited to

  * Automata theory and formal languages;
  * Principles and semantics of programming languages;
  * Theories of concurrency, mobility and reconfiguration;
  * Logics and their applications;
  * Software architectures, their models, refinement and verification;
  * Relationship between software requirements, models and code;
  * Program static and dynamic analysis and verification;
  * Software specification, refinement, verification and testing;
  * Model checking and theorem proving;
  * Models of object and component systems;
  * Coordination and feature interaction;
  * Integration of theories, formal methods and tools for
    engineering computing systems;
  * Service-oriented architectures: models and development methods;
  * Models of concurrency, security, and mobility;
  * Theory of distributed, grid and cloud computing;
  * Real-time, embedded, hybrid and cyber-physical systems;
  * Type and category theory in computer science.

PAPER SUBMISSION

As for the past editions, the proceedings of ICTAC 2014 will be 
published by Springer in the series Lecture Notes in Computer Science 
(LNCS) and will be available at the colloquium. Special issue of few 
journals with extended version of selected papers from ICTAC 2014 is 
under negotiation. Submissions to the colloquium must not have been 
published or be concurrently considered for publication elsewhere. All 
submissions will be judged on the basis of originality, contribution to 
the field, technical and presentation quality, as well as their 
relevance to the conference.

Regular Papers should not exceed 18 pages in LNCS format (see 
http://www.springer.de/comp/lncs/authors.html for details). Papers must 
be submitted by using www.easychair.org/conferences/?conf=ictac2014.

IMPORTANT DATES:

Abstract submission: 16 March 2014
Submission deadline: 23 March 2014
Paper notification:  30 May 2014
Revised/final paper: 14 June 2014

GENERAL CHAIRS

Gabriel Ciobanu, Romanian Academy, ICS, Iasi
Florentin Ipate, University of Bucharest, Romania

PC CHAIRS

Gabriel Ciobanu, Romanian Academy, ICS, Iasi, Romania
Dominique Mery, LORIA, Universite de Lorraine, France

PROGRAM COMMITTEE

Yamine Ait-Ameur, IRIT, ENSEIHT, France
Farhad Arbab, CWI and Leiden University, The Netherlands
Michael Butler, University of Southampton, UK
Ana Calvacanti, University of York, UK
Jeremie Chalopin, CNRS, France
Zhenbang Chen, National University of Defense Technology, China
Maximiliano Cristia, Faculty of Exact Sciences, Argentina
David Deharbe, Universidade Federal do Rio Grande do Norte, Brazil
Rocco De Nicola, IMT Lucca, Italy
Jose Luiz Fiadeiro, Royal Holloway, University of London, UK
John Fitzgerald, Newcastle University, UK
Simon Gay, University of Glasgow, UK
Dimitra Giannakopoulou, NASA Ames, USA
Stefania Gnesi, ISTI-CNR, Italy
Lindsay Groves, Victoria University of Wellington, New Zealand
Geoff Hamilton, Dublin City University, Ireland
Ian J. Hayes, University of Queensland, Australia
Rob Hierons, Brunel University, UK
Jane Hillston, University of Edinburgh, UK
Ross Horne, Romanian Academy, Iasi, Romania
Zhenjiang Hu, National Institute of Informatics, Japan
Florentin Ipate, University of Bucharest, Romania
Tudor Jebelean, Johannes Kepler University, Austria
Cliff Jones, Newcastle University, UK
Lila Kari, University of Western Ontario, Canada
Jetty Kleijn, Leiden University, The Netherlands
Maciej Koutny, Newcastle University, UK
Yassine Lakhnech, VERIMAG, France
Kim G. Larsen, Aalborg University, Denmark
Insup Lee, University of Pennsylvania, USA
Axel Legay, INRIA, France
Martin Leucker, University of Lubeck, Germany
Zhiming Liu, UNU-IIST, Macau, China
Marius Minea, Politehnica University of Timisoara, Romania
Victor Mitrana, University of Bucharest, Romania
Rosemary Monahan, National University of Ireland, Ireland
Mohammed Mosbah, LABRI, University of Bordeaux, France
Tobias Nipkow, Technical University Munich, Germany
Manuel Nunez, Universidad Complutense de Madrid, Spain
Paritosh Pandya, Tata Institute of Fundamental Research, India
Jun Pang, University of Luxembourg, Luxembourg
Corina Pasareanu, NASA Ames, USA
Shengchao Qin, University of Teesside, UK
Antonio Ravara, Universidade Nova de Lisboa, Portugal
Grigore Rosu, University of Illinois at Urbana Champaign, USA
Augusto Sampaio, Federal University of Pernambuco, Brasil
Pierre-Yves Schobbens, Universite de Namur, Belgium
Emil Sekerinski, McMaster University, Canada
Natarajan Shankar, SRI International, USA
Viorica Sofronie-Stokkermans, Max Planck Institute, Germany
Gheorghe Stefanescu, University of Bucharest, Romania
Andrzej Tarlecki, Warsaw University, Poland
Elena Troubitsyna, Abo Akademi University, Finland
Emilio Tuosto, University of Leicester, UK
Martin Wirsing, Ludwig-Maximilian University of Munich, Germany
Burkhart Wolff, Universite de Paris-Sud, France
Jim Woodcock, University of York, UK
Fatiha Zaidi, Universite de Paris-Sud, France
Naijun Zhan, Chinese Academy of Sciences, China
Jianjun Zhao, Shanghai Jiao Tong University, China
Huibiao Zhu, East China Normal University, China

                              STEERING COMMITTEE

Ana Cavalcanti, University of York, United Kingdom
John Fitzgerald, Newcastle University, UK
Martin Leucker, University of Luebeck, Germany
Zhiming Liu, UNU-IIST, Macao, China
Tobias Nipkow, Technical University Munich, Germany
Augusto Sampaio, Federal University of Pernambuco, Brasil
Natarajan Shankar, SRI International, USA

**********************************************************************
This call for papers and additional information about the conference can
be found on the ICTAC 2014 web page http://fmi.unibuc.ro/ictac2014/.
For information regarding the conference and other queries, you can use
the conference email address: ictac2014@fmi.unibuc.ro
**********************************************************************

Sunday, October 13, 2013

Correct-by-Construction Development of Dependable Systems

http://2013.dsn.org/tutorial-a-romanovsky/

Investigation of the B Method

http://www-users.cs.york.ac.uk/~zeyda/downloads/mscthesis_zeyda.pdf

REVERSIBLE COMPUTATIONS IN B

http://www-users.cs.york.ac.uk/~zeyda/downloads/phdthesis_zeyda.pdf

Formal Development of System of Systems

http://www.hindawi.com/isrn/software.engineering/2013/457837/

A rigorous reasoning about model transformations using the B method

http://hal.inria.fr/hal-00853720

ICFEM 2013, 15th International Conference on Formal Engineering Methods

http://www.cs.auckland.ac.nz/research/conferences/icfem2013/index.php

Call for Papers: Formal Methods 2014 (FM 2014), Singapore, May 14-16, 2014


Call for Papers: Formal Methods 2014 (FM 2014), Singapore, May 14-16, 2014

CALL FOR PAPERS:
Formal Methods 2014 (FM 2014)
19th International Symposium on Formal Methods
Singapore, May 14-16, 2014
http://www.comp.nus.edu.sg/~pat/FM2014/

FM 2014 is the nineteenth in a series of symposia organized by
Formal Methods Europe, an independent association whose aim is
to stimulate the use of, and research on, formal methods for
software development. The symposia have been notably successful
in bringing together innovators and practitioners in precise
mathematical methods for software and systems development,
industrial users, as well as researchers. Submissions are
welcomed in the form of original papers on research and
industrial experience, proposals for workshops and tutorials,
entries for the exhibition of software tools and projects, and
reports on ongoing doctoral work.

SCOPE AND TOPICS

It will have the goal of highlighting the development and
application of formal methods in connection with a variety of
disciplines such as medicine, biology, human cognitive modeling,
human automation interactions and aeronautics, among others. FM
2014 particularly welcomes papers on techniques, tools and
experiences in interdisciplinary frameworks, as well as on
experience with practical applications of formal methods in
industrial and research settings, experimental validation of
tools and methods as well as construction and evolution of
formal methods tools. The broad topics of interest for FM 2014
include but are not limited to:

Interdisciplinary formal methods: techniques, tools and
experiences demonstrating formal methods in interdisciplinary
frameworks.

Formal methods in practice: industrial applications of formal
methods, experience with introducing formal methods in industry,
tool usage reports, experiments with challenge problems. Authors
are encouraged to explain how the use of formal methods has
overcome problems, lead to improvements in design or provided
new insights.

Tools for formal methods: advances in automated verification and
model-checking, integration of tools, environments for formal
methods, experimental validation of tools. Authors are
encouraged to demonstrate empirically that the new tool or
environment advances the state of the art.

Role of formal methods in software and systems engineering:
development processes with formal methods, usage guidelines for
formal methods, method integration. Authors are encouraged to
demonstrate that process innovations lead to qualitative or
quantitative improvements.

Theoretical foundations: all aspects of theory related to
specification, verification, refinement, and static and dynamic
analysis. Authors are encouraged to explain how their results
contribute to the solution of practical problems.

PAPER SUBMISSION

Papers will be evaluated by at least three members of the Program
Committee. They should be in Springer LNCS format and describe,
in English, original work that has not been published or submitted
elsewhere. Papers should be submitted through the FM 2014
EasyChair web site.

We solicit two categories of papers:

Regular papers should not exceeding 15 pages (including
appendices), describing fully developed work. Authors of papers
reporting experimental work are strongly encouraged to make their
experimental results available for use by reviewers. Similarly,
case study papers should describe significant case studies and
the complete development should be made available for use by
reviewers.

Tools papers of a maximum of 4 pages should describe an
operational tool and its contributions; 2 additional pages of
appendices are allowed that will not be included in the
proceedings. Tool papers should explain enhancements made
compared to previously published work. A tool paper need not
present the theory behind the tool but can focus more on its
features, and how it is used, with screen shots and examples.
Authors of tools papers should make their tool available for
use by reviewers.

Industry track papers (with a different deadline) should not
exceeding 15 pages (including appendices), describing industrial
applications of formal methods, experience with introducing
formal methods in industry, tool usage reports, experiments with
challenge problems. Authors are encouraged to explain how the
use of formal methods has overcome problems, lead to improvements
in design or provided new insights.

IMPORTANT DATES

Abstract due: November 7, 2013
Full papers due: November 14, 2013
Acceptance / Rejection Notification: February 1, 2014
Industry Track Submission: January 16, 2014
Industry Track Notification: February 16, 2014
Camera-ready: February 25, 2014
Main Conference Date: May 14-16, 2014
Tutorial / Workshops Date: May 12-13, 2014

CALL FOR TUTORIALS, WORKSHOPS and DOC SYMPOSIUM

The organizing committee of FM 2014 thus invites proposals for
half- or full-day tutorials in the broad area of formal methods.
Proposals from industry practitioners or academics are very
welcome; proposals for tutorials on applications of formal
methods to challenging problems are particularly welcome. All
tutorials should focus on providing participants with the
opportunity to learn new techniques, new application domains,
and insightful uses of formal methods. Details on the call for
tutorials can be found at http://www.comp.nus.edu.sg/~pat/FM2014/cft.html

We are also inviting people to submit proposals for workshops.
The purpose of the workshops is to provide an informal setting
for workshop participants to discuss technical issues, exchange
research ideas, and to discuss and/or demonstrate applications.
These workshops may be driven by fundamental academic interests
or by needs from specific application domains. We encourage a
diversity of workshops relating to different varieties of formal
models. Details on the call for workshops can be found at
http://www.comp.nus.edu.sg/~pat/FM2014/cfp4w.html

A Doctoral Symposium will be held on 12-13th May in conjunction
with the FME Symposium FM2014. This aims to provide a helpful
environment in which selected doctoral students can present and
discuss their ongoing work, meet other students working on
similar topics and receive helpful advice and feedback from a
panel of researchers and academics. Details on the call for
doctoral symposium can be found at
http://www.comp.nus.edu.sg/~pat/FM2014/cfd.html

ORGANIZATION COMMITTEE

General Chair
Jin Song Dong, National University of Singapore, Singapore.

Program Committee Co-Chairs
Cliff B Jones, Newcastle University, United Kingdom.
Pekka Pihlajasaari, Data Abstraction (Pty) Ltd, South Africa.
Jun Sun, Singapore University of Technology and Design, Singapore.

Doc Symposium Co-Chair
Annabelle McIver, Macquarie University, Australia.

Workshop Chair
Shengchao Qin, University of Teesside, United Kingdom.

Publicity Chair
Jonathan Bowen, London South Bank University, United Kingdom.
Kenji Taguchi, AIST, Japan.

Tutorial Chair
Richard Paige, University of York, United Kingdom.

Program Committee - Main Track

Bernhard Aichernig, Austria.
Richard Banach, School of Computer Science, University of Manchester,
United Kingdom.
Juan Bicarregui, Rutherford Appleton Laboratory, United Kingdom.
Andrew Butterfield, Trinity College Dublin, Northern Ireland.
Ana Cavalcanti, United Kingdom.
Marsha Chechik, University of Toronto, Canada.
Yu-Fang Chen, Academia Sinica, Taiwan.
Wei-Ngan Chin, National Univ of Singapore, Singapore.
Dino Distefano, University of London, United Kingdom.
Jim Davies, University of Oxford, United Kingdom.
Frank De Boer, CWI, Netherlands.
José Luiz Fiadeiro, Royal Holloway, University of London, United Kingdom.
John Fitzgerald, Newcastle University, United Kingdom.
Marie-Claude Gaudel, LRI, Univ. Paris-Sud and CNRS, France.
Jaco Geldenhuys, Stellenbosch University, South Africa.
Dimitra Giannakopoulou, NASA Ames, United States.
Stefania Gnesi, ISTI-CNR, Italy.
Lindsay Groves, Victoria University of Wellington, New Zealand.
Stefan Gruner, University of Pretoria, South Africa.
Anne E. Haxthausen, Technical University of Denmark, Denmark.
Ian J. Hayes, University of Queensland, Australia.
Constance Heitmeyer, Naval Research Laboratory, Washington DC 20375,
United States.
Jane Hillston, University of Edinburgh, United Kingdom.
Shinichi Honiden, National Institute of Informatics, Japan.
Daniel Jackson, MIT, United States.
Cliff Jones, Newcastle University, United Kingdom.
Rajeev Joshi, Laboratory for Reliable Software, Jet Propulsion
Laboratory, United States.
Peter Gorm Larsen, Aarhus School of Engineering, Denmark.
Axel Van Lamsweerde, Universite Catholique de Louvain, Belgium.
Gary T. Leavens, University of Central Florida, United States.
Yves Ledru, Laboratoire d'Informatique de Grenoble - Université Joseph
Fourier, France.
Michael Leuschel, University of Düsseldorf, Germany.
Brendan Mahony, DSTO, Australia.
Tom Maibaum, McMaster University, Canada.
Annabelle McIver, Macquarie University, Australia.
Dominique Mery, Université de Lorraine, LORIA, France.
Peter Müller, ETH Zürich, Switzerland.
Tobias Nipkow, TU München, Germany.
Colin O'Halloran, QinetiQ Ltd, United Kingdom.
Jose Oliveira, Universidade do Minho, Portugal.
Pekka Pihlajasaari, Data Abstraction (Pty) Ltd, South Africa.
André Platzer, Carnegie Mellon University, United States.
Zongyan Qiu, Peking University, China.
Ken Robinson, The University of New South Wales, Australia.
Andreas Roth, SAP Research, United States.
Abhik Roychoudhury, National University of Singapore, Singapore.
Augusto Sampaio, Federal university of Pernambuco, Brazil.
Steve Schneider, University of Surrey, United Kingdom.
Emil Sekerinski, McMaster University, Canada.
Ketil Stoelen, SINTEF, Norway.
Jun Sun, Singapore University of Technology and Design, Singapore.
Jing Sun, The University of Auckland, New Zealand.
Xiaoyu Song, Portland State University, United States.
Marcel Verhoef, Chess, Netherlands.
Willem Visser, Stellenbosch University, South Africa.
Chao Wang, Virginia Tech, United States.
Alan Wassyng, McMaster University, Canada.
Pamela Zave, AT&T Laboratories--Research, United States.
Lijun Zhang, Technical University of Denmark, Denmark.

Program Committee - Industry Track

Jun Sun, Singapore University of Technology and Design, Singapore.
Cliff Jones, Newcastle University, United Kingdom.
Pekka Pihlajasaari, Data Abstraction (Pty) Ltd, South Africa.
Michael Holloway, NASA, United States.
Ralf Huuck, NICTA, Australia.
Ewen Denney, SGT/NASA Ames, United States.
Jim Grundy, Intel Corporation, United States.
Hongjun Zheng, MathWorks, United States.
Wolfgang Grieskamp, Google, United States.
Cristina Cifuentes, Oracle, Australia.
Jon Burton, Praxis, United Kingdom.

_______________________________________________
events mailing list
events@fmeurope.org
http://fmeurope.hosting.west.nl/mailman/listinfo/events

Friday, October 4, 2013

Case study, the landing system

http://www.irit.fr/ABZ2014/landing_system.pdf

Cours et Travaux dirigés de spécification

http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/spec1/Spec1sommaire.html

The first "B International Conferences"

http://www.lina.sciences.univ-nantes.fr/coloss/members/habrias/ConfZetBdeNantes/ConfZBNantes.html

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:

Thursday, August 29, 2013

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

http://inscriptions.js.univ-nantes.fr/?id=CL03

Logiciels de qualité : modélisation et vérification