http://www.avocs2013.org.uk

11-13th September, 2013
University of Surrey, UK

Submission (abstract for full paper): 31st May 2013
Submission (full papers): 7th June 2013

FME is sponsoring three students bursaries for the event.

Next to its main FM conference series, FME sponsors other events related to formal methods. Typically invited talks are sponsored. Details about sponsorship can be found in our Guide to FME Sponsorship.

ABSTRACTS AND SLIDES OF THE INVITED TALKS

prof. dr. Frank S. de Boer, CWI and LIACS (NL)

Run-Time Assertion Checking of Data- and Protocol-Oriented Properties of Java Programs

Run-time assertion checking is one of the most useful techniques for detecting faults, and can be applied during any program execution context, including debugging, testing, and production.  But in general it is limited to checking state-based properties.  We introduce SAGA, a general framework that provides a smooth integration of the specification and the run-time checking of both data- and protocol-oriented properties of Java classes and interfaces. Download the presentation Run-Time Assertion Checking in Java.

dr. Marieke Huisman, Universiteit Twente (NL)

Verification of Concurrent Data Structures

In earlier work, we developed a variant of permission-based separation logic that is particularly suited to reason about multithreaded Java programs with dynamic thread creation and termination, and reentrant locks. This talk discusses how within the context of the VerCors project, we extend this approach to make it suitable to specify and verify concurrent data structures. In particular, we will discuss the following topics:

• a natural generalisation of the lock specification approach to other synchronisation mechanisms from the Java API;
• the use of histories to describe functional behaviour of concurrent data structures; and
• specification and verification of lock-free data structures.  We will also discuss the architecture of the tool set supporting our approach.

Finally, we will also present how permission-based separation logic is also suitable to reason about programs in a different concurrency setting, such as GPU kernels written in OpenCL. Download the presentation Verification of Concurrent Datastructures.

dr. Ana Cavalcanti, University of York (UK)

Safety-Critical Java Programs from Circus Models

Safety-Critical Java (SCJ) is a novel version of Java that addresses issues related to real-time programming and certification of safety-critical applications. We present a technique that reveals the issues involved in theformal verification of an SCJ program, and provides guidelines for tackling them in a refinement-based approach.

It is based on Circus, a combination of well established notations: Z, CSP, Timed CSP, and object orientation. We cater for the specification of timing requirements and their decomposition towards the structure of missions and event handlers of SCJ. We also consider the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. We present a refinement strategy and a Circus variant that captures the essence of the SCJ paradigm. Download the presentation Safety-Critical Java in Circus.

prof. Michael Jackson, Open University and University of Newcastle (UK)

Formalism and Intuition in Software Development

Henri Poincare recognised the importance of two tools of human intellect: science and intuition. In software development we may recognise them in formal and informal techniques and approaches. This talk briefly discusses their different natures and virtues, and suggests a relationship in which each can play its part most effectively. Download the presentation Formalism and Intuition in Software Development.

AGENDA OF THE FME BUSINESS MEETING

1. Welcome and agree upon agenda (chair)
2. Minutes of the previous meeting and review of actions (secretary)
3. Annual report for 2012 (Secretary)
4. Financial report for 2012 (Treasurer)
5. Report by Independent Financial Examiners (Treasurer)
6. Elections (chair)
   - Treasurer, to serve until 2016
   - Independent Financial Examiner, for 2013 and 2014
7. Plan for 2013 (chair)
8. Budget 2013, including sponsorships (Treasurer)
9. Symposia (S. Gnesi)
   - Final report on FM 2012 (Paris)
   - Status report on FM 2014 (Singapore)
10. FME Education Subgroup (Chair)
11. FME web-site / Electronic publications (B. Aichernig)
12. FormaliSE workshop at ICSE (N. Plat / S. Gnesi)
13. SCORE student competition at ICSE (M. Rossi)
14. Date and place of next meeting (Secretary)
15. Any Other Business (Chair)

Documents for the AGM

• Minutes of last meeting
• FME activities report
• Publications report
• FME Plans 2013

LOCAL ORGANISATION

• Erik de Vink, Technical University Eindhoven and CWI
• Nico Plat, West Consulting B.V.
• Marcel Verhoef, Chess Embedded Technology International B.V.

Details will follow.

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/

Papers due: February 7, 2013

INTRODUCTION
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.

Formal methods (FMs) are intended to provide the means for greater precision in both thinking and documenting the preliminary stage of the software creation process. When done well, this can aid all aspects of software creation: user requirement formulation, implementation, verification/testing, and the creation of documentation. However, the maturing of formal techniques into real-life software engineering involves providing notations and tools that are readily understood and used by practitioners, and the integration of such tools with activities that are far from the unrealistic assumptions that characterized some earlier research in 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 couldbe 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.

AREAS OF INTEREST include but are not limited to:

• integration of FMs in the software development 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

THE PROGRAM will start with an invited speaker (to be announced), 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 Conference Proceedings Format. They will be published as part of the (electronic) proceedings 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 theworkshop submission website at the following URL:

https://www.easychair.org/account/signin.cgi?conf=formalise2013

All submissions will be reviewed by three PC members. They will be judged on the basis of their clarity, relevance, originality, and contribution.

IMPORTANT DATES

• 7 February 2013: submission deadline for workshop papers
• 28 February 2013: notification of acceptance/rejection to authors
• 7 March 2013: camera-ready copy deadline for workshop papers
• 25 May 2013: FormaliSE workshop held in San Francisco, USA

OC/PC CHAIRS are Stefania Gnesi (ISTI-CNR, Italy) and Nico Plat (West Consulting BV, The Netherlands). The OC/PC Chairs can be reached via e-mail: oc@formalise.org. If you intend to submit a paper you are encouraged to inform us in advance.

THE PROGRAM COMMITTEE consists of:

• 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 Garfinkel (Carnegie Mellon University, USA)
• Patrick Heymans (University of Namur, Belgium, and INRIA, France)
• Alessandro Fantechi (Università di Firenze, Italy)
• Mike Hinchey (Lero, Ireland)
• Axel van Lamsweerde (University of Louvain. Belgium)
• Peter Gorm Larsen (Engineering College of Aarhus, 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)

]]> http://www.fmeurope.org/?feed=rss2&p=446 http://www.fmeurope.org/?p=445 http://www.fmeurope.org/?p=445#comments Fri, 19 Oct 2012 08:23:58 +0000 admin http://www.fmeurope.org/?p=445 The 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012) was held on 18-20th September 2012 at the University of Bamberg, Germany. AVoCS is dedicated to subjects of automated verification, including model checking, theorem proving, abstract interpretation and refinement concepts, interpreted in a broad and inclusive manner. The workshop series contributes to the discussion and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems.

The workshop programme spanned three days and was composed of six sessions:

• Model Checking & Applications
• Timed Systems
• Case Studies
• TLA, CSP & B
• Stochastic & Probabilistic Model checking
• Concurrency & Logic

The workshop also featured four keynote presentations that were eloquently delivered by experts in their respective fields:

• Jon Holt: The Great Escape - Model-based Testing for Safety-Critical Systems
• Michael Goldsmith: Inside FDR
• Christoph Weidenbach: Automated Reasoning by Superposition
• Jaco van de Pol: Multi-core and/or Symbolic Model Checking

In addition to the well organised talks and coffee breaks, the conference dinner offered an intimate atmosphere for further discussions, with an excellent view over the 1100 year old city of Bamberg.

The preliminary workshop proceedings were available at the workshop and contain the regular and short papers selected by the PC as well as the short papers accompanying the keynote presentations. Revised versions of the regular papers will be published in the Electronic Communications of the European Association of Software Science and Technology (ECEASST).

The organizers are grateful for the generous support of Formal Methods Europe.

The general chair responsible for the event is Jin Song Dong. The local chair is Yang Liu, NTU, Singapore.

The PC Co-Chairs responsible for the technical program are

• Cliff B. Jones: Newcastle University, UK
• Pekka Pihlajasaari: Data Abstraction (Pty) Ltd., South Africa
• Jun Sun: Singapore University of Technology and Design, Singapore

Important Dates:

Abstract due: November 7, 2013

Full papers due: November 14, 2013

Industry Track Submissions: January 16, 2014

The Preliminary Call for Papers is available for download.

More details can be found on the website of FM 2014.

The FM conference series is the main event on formal methods organized by the FME organization. A list of past FM symposia can be found here.

(Photo: williamcho)

CALL FOR PARTICIPATION

FM 2012: 18TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

August 27-31, 2012

CNAM, Paris, France

http://fm2012.cnam.fr/

CONFERENCE SCOPE

FM 2012 is the eighteenth 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.

The special theme of FM 2012 is Interdisciplinary Formal Methods, with a 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.

INVITED TALKS

We are honored to have three invited speakers whose talks emphasized the special theme: the awareness of the community to the fact that formal methods live in the intersection of disciplines; formal methods research must also consider how to increase its industrial impact.

Martin Abadi - Software Security: A Formal Perspective

Asaf Degani - Formal Methods in the Wild: Trains, Planes, & Automobiles

Alan Wassyng - Who are we and what are we doing here?

The FM2012 Conference programme is available online:

http://fm2012.cnam.fr/fm2012/conferenceprogram.php

The symposium will also host several associated events: Industry day, workshops, tutorials, Doctoral Consortium and a verification competition. For further information on the associated events, see links from the main website under:  http://fm2012.cnam.fr/

CONFERENCE VENUE

FM 2012 will be held at The Conservatoire National des Arts et Métiers (Le Cnam) in the center of Paris. For further infos, see: http://fm2012.cnam.fr/fm2012/localinformation.php

GENERAL CHAIRS

Kamel Barkaoui, CEDRIC, CNAM, Paris, France

Béatrice Bérard,  LIP6, UPMC, Paris, France

PC CHAIRS

Dimitra Giannakopoulou, NASA Ames, Research Center,Moffett Field, USA

Dominique Méry, LORIA, Université Henri Poincaré Nancy 1, France

PROGRAMME COMMITTEE

See: http://fm2012.cnam.fr/fm2012/programcommittee.php

WORKSHOPS, 27-28 August 2012

Chairs: Nihal Pekergin, Laure Petrucci, Tayssir Touili, France

See: http://fm2012.cnam.fr/fm2012/workshops.php

INDUSTRY DAY, 30 June 2011

Chairs: Isabelle Perseil, Karim Djouani, Thierry Lecomte, Bruno Monsuez, France

See: http://fm2012.cnam.fr/fm2012/industryday.php

TUTORIALS, 27-28 August 2012

Chairs: Serge Haddad, Fabrice Kordon, France

See: http://fm2012.cnam.fr/fm2012/tutorials.php

DOCTORAL SYMPOSIUM, 27 August 2012

Chairs:  Christine Choppy, David Delayahe, Kaïs Klaï, France

See: http://fm2012.cnam.fr/fm2012/doctoralsymposium.php

VERIFICATION COMPETITION, 29-30 August 2012

Chairs: Marieke Huisman, The Netherlands, Vladimir Klebanov, Germany, Rosemary Monahan, Ireland

See: http://fm2012.cnam.fr/fm2012/verificationcompetition.php

PUBLICITY CHAIRS: Hanna Klaudel, Frederic Lemoine, Franck Pommereau , Olivier Pons, France

SOCIAL EVENTS

Each day: coffee breaks and sit-down lunches offer ample time for interaction and networking.

Wednesday 29 August evening: Welcome reception in the Chapel Saint-Martin-des-Champs of “Arts et Métiers” Museum

Thursday 30 August evening: Conference dinner on August 30th on the Bateau Mouche “Capitaine Fracasse” on the Seine in Paris

All attendees of FM 2012 Symposium will have, during FM 2012 week, access to the Cnam “Arts et Métiers” Museum.

Further information See: http://fm2012.cnam.fr/fm2012/socialevents.php

REGISTRATION

Information and online booking: http://fm2012.cnam.fr/fm2012/registration.php

ACCOMODATION

Information on hotels is under: http://fm2012.cnam.fr/fm2012/localinformation.php

Please make sure you book accommodation as soon as possible. Paris will be very busy in that week.

For more info and latest updates see the conference web site at < http://fm2012.cnam.fr/>.

We look forward to seeing you in Paris in August!

Organizing Committee FM 2012