Venue: Microsoft Research Cambridge
Dates: 21-22 September 2017
Organisers: Philippa Gardner (Imperial), Markulf Kohlweiss (MSR Cambridge), Mike Gordon (Cambridge University), Graham Steel (INRIA and Cryptosense, Paris).
Almost a hundred participants attended the Fifth Workshop on Formal Methods and Tools for Security (FMATS5), held on 21-22 September at Microsoft Research Cambridge. The workshop, now on its fifth year, was attended by researchers, PhD students, industrialists and government employees with a common interest in formal methods and verification. The programme included 19 specialist talks, poster presentations and a session of short talks for PhD students, RAs and industrialists to introduce themselves to each other and the audience.
For a list of the talks please see FMATS5’s programme.
Slides are available for the following talks:
- Mark Batty, University of Kent, Industrial concurrency specification for C/C++
- Rod Chapman, Protean Code Ltd., Sanitizing Sensitive Data: How to get it Right (or at least Less Wrong…)
- James Cheney, University of Edinburgh (VeTSS’17), Language, Data, and Security
- Simon Foster (York, VeTSS’17) Isabelle/UTP: A Verification Toolbox for Unifying Theories
You can also see photos of the two days on the FMATS5 Flickr page.
FMATS
The Workshop on Formal Methods and Tools for Security (FMATS), inspired by the grand challenge of software verification, was established in 2011 by Professor Mike Gordon of the University of Cambridge, with the aim of bringing together academia, industry and government employees interested in an effort to properly understand and address the challenges in applying formal methods to security. Since then, three more FMATS workshops have been held in 2013, 2014, and 2015, all at Microsoft Research Cambridge, with Philippa Gardner taking over as lead organiser in 2015.
In place of FMATS in 2016, Gardner and Gordon, together with Greg Morrisett (Cornell), Peter O’Hearn (Facebook London) and Fred Schneider (Cornell), organised the Royal Society Scientific and Discussion Meeting, and an associated specialist meeting at Imperial College London, on Verified Trustworthy Software Systems. The aim of these meetings was to bring together academics, industrial experts and government scientists, united by their interest in verification, to identify key challenges in establishing verification at the heart of the software design process.
These meetings spearheaded the successful application for the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and directed by Gardner. FMATS is now co-organised with VeTSS. You can find details of previous editions of FMATS here.
Programme
FMATS traditionally attracts a wide audience, including UK academic researchers, PhD Students, industrialists and government employees. The two-day workshop comprises invited talks addressing key research topics from the field of formal methods and their application to security, with the aim of fostering discussion between all participants.
One important aim is to foster dialogue between the PhD students, RAs and industry. The transition from either PhD student or RA to industry is known to be difficult, with each individual essentially making it up as they go along. One hope is that, through FMATS and VeTSS, it will be possible to build up a level of understanding of the opportunities out there for analysis and verification enthusiasts in the industrial sector.