« All Events

  • This event has passed.

Third Workshop on Formal Methods And Tools for Security (FMATS3)

May 1, 2014 - May 2, 2014

FMATS3 was held at Microsoft Research Cambridge on 1st and 2nd May 2014. This year we had additional talks from the individual projects affiliated to the Research Institute in Automated Program Analysis and Verification (RI2).  The event was attended by 47 participants comprising researchers from academia, industry and government and included talks on 16 different topics (see final programme). On the 2nd day, we had a poster session along with bite-size introductions from nine winners of the “PhD Prizes”. In the  discussion session on the future of the FMATS workshop, it was agreed that the FMATS community should be opened to other complementary networks like CryptoForma and adopt ideas from other similar events like NSA’s HCSS conference.

The future organisation of FMATS will be led by the Director of RI2, Professor Philippa Gardner of Imperial College London.

For previous FMATS webpages, click here


Final Programme

Morning of Thursday May 1

    08:30-09:30   Tea, coffee and pastries
    09:30-09:35   Welcome to FMATS and Microsoft Research Cambridge by Andy Gordon
    09:35-10:30   Robert Watson

    10:30-11:00   Coffee break

    11:00-11:30   Compositional Security Analysis for Binaries [RI2 Project]
    11:30-12:00   App Guarden: Resilient Application Stores [RI2 Project]
    12:00-12:30   Program Verification Techniques for Understanding Security Properties of Software [RI2 Project]

    12:30-14:00   Lunch

Afternoon of May 1

    14:00-14:30   Graham Steel (talk about Cryptosense)
    14:30-15:00   Rod Chapman (on the design of SPARK2014)
    15:00-15:30   Konrad Slind (High Performance Regular Expression Processing for Cross-Domain Systems-
                               -with High Assurance Requirements)

    15:30-16:00   Tea break

    16:00-16:30   Matt Lewis (on work related to acceleration and exploit generation)
    16:30-17:00   Paul Thomson (Concurrency Testing Using Schedule Bounding: an Empirical Study)
    17:00-17:30   Robert Künnemann (on the MAC In The Box project)

    18:30-21:00   Workshop dinner at the Curry Queen (directions)

Morning of Friday May 2

    08:30-09:30   Coffee, informal discussions and poster viewing (click here for Joeri's slide)
    09:30-10:30   Andrey Rybalchenko (Horn Constraint Solving for Program Verification and Synthesis)

    10:30-11:00   Coffee break

    11:00-11:30   Andreas Holzer (CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations)
    11:30-12:00   Marco Gaboardi (on proving differential privacy by Hoare Logic)
    12:00-12:30   Will Harwood (to talk about Silicon Safe Ltd, a startup)

    12:30-14:00   Lunch

Afternoon of May 2
    14:00-14:30   Certified Verification of Client-Side Web Programs [RI2 Project]
    14:30-15:00   SeMaMatch: Semantic Malware Matching [RI2 Project]
    15:00-15:30   Tea break

    15:30-16:30   Discussion on RI2 and the future of the FMATS workshops (chaired by Philippa Gardner)
    16:30         End of Workshop.


May 1, 2014
May 2, 2014


Philippa Gardner, Markulf Kohlweiss, Mike Gordon, Andy Jackson, Graham Steel


Microsoft Research Cambridge