The Formal Methods Europe Annual General Meeting 2013 and Celebration of Formal Methods, was held on Friday 8 March 2013 at CWI, Amsterdam, The Netherlands. Four invited speakers gave presentations on current research in a day that was both enjoyable and informative.
ABSTRACTS AND SLIDES OF THE INVITED TALKS
[prof. dr. Frank S. de Boer](http://homepages.cwi.nl/~frb/), 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](http://wwwhome.ewi.utwente.nl/~marieke/),
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](http://www-users.cs.york.ac.uk/~alcc/), 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[ ]{style=“mso-spacerun: yes;"}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[ ]{style=“mso-spacerun: yes;"}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
- Welcome and agree upon agenda (chair)
- Minutes of the previous meeting and review of actions (secretary)
- Annual report for 2012 (Secretary)
- Financial report for 2012 (Treasurer)
- Report by Independent Financial Examiners (Treasurer)
- Elections (chair)
- Treasurer, to serve until 2016
- Independent Financial Examiner, for 2013 and 2014
- Treasurer, to serve until 2016
- Plan for 2013 (chair)
- Budget 2013, including sponsorships (Treasurer)
- Symposia (S. Gnesi)\
- Final report on FM 2012 (Paris)
- Status report on FM 2014 (Singapore)
- Final report on FM 2012 (Paris)
- FME Education Subgroup (Chair)
- FME web-site / Electronic publications (B. Aichernig)
- FormaliSE workshop at ICSE (N. Plat / S. Gnesi)
- SCORE student competition at ICSE (M. Rossi)
- Date and place of next meeting (Secretary)
- Any Other Business (Chair)
Documents for the AGM
LOCAL ORGANISATION
- Erik de Vink, Technical University Eindhoven and CWI
- Nico Plat, West Consulting B.V.
- Marcel Verhoef, Chess Embedded Technology International B.V.
