FMATS4 was successfully held at Microsoft Research Cambridge on 11 and 12 June 2015. The event was attended by more than 65 participants comprising researchers, industrialists and government employees,  and included specialist talks on 15 different topics (see final programme). In addition to the specialist talks, we had bite-size introductions from six winners of the “PhD Prizes” and an open-discussion on the next steps.

Venue: Microsoft Research Cambridge (map)

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

FMATS4 is supported by the Research Institute in Automated Program Analysis and Verification funded by GCHQ, EPSRC and BIS.

Final Programme

Thursday June 11

    09:30-09:55   Tea, coffee and pastries
	
    09:55-10:00   Welcome to FMATS4 by Philippa Gardner (Imperial College London)
    10:00-11:00   Keynote by Daniel Kroening (University of Oxford), 
	              Title: DANGER Invariants

    11:00-11:30   Coffee break

    11:30-12:00   Pasquale Malacaria (QMUL), Talk on analysis of Heartbleed 
	              [RI Project] Compositional Security Analysis for Binaries
				  
    12:00-12:30   Brad Karp (UCL), Title: Practical Privacy for Web Users with COWL 
	              [RI Project] Program Verification Techniques 
				  
    12:30-13:00   David Clark (UCL), Title: Malware Detection through Pre Static Analysis 
	              [RI Project] SeMaMatch: Semantic Malware Matching
	
    13:00-14:00   Lunch

    14:00-14:30   Dalal Alrajeh (Imperial College London),
	              Title: Reasoning about Crime through verification and rule-based learning
    14:30-15:00   Hannes Mehnert (University of Cambridge), Talk on safe TLS stack work 
    15:00-15:30   Graham Steel (Cryptosense), Title: Crypto Application Analysis 

    15:30-16:00   Tea break

    16:00-16:30   Igor Muttik (McAfee), Title: Recognising and tracking code reuse 
	              [RI Project] App Guarden: Resilient Application Stores
				  
    16:30-17:15   5-min talks by PhD students (Prize winners)
                  [Dehnel, Filaretti, Franzen, Kuchta, Neville, Repel]

    18:30-22:00   Drinks Reception and Workshop Dinner at Westminster College
		
Friday June 12

    08:30-09:00   Coffee, informal discussions and poster viewing
	
    09:00-10:00   Keynote by Gilles Barthe (IMDEA Software Institute), 
	              Title: Computer-Aided Cryptography
    10:00-10:30	  Markulf Kohlweiss (Microsoft Research),
	              Title: (mi)TLS 1.3: can cryptography, formal methods, and applied security be friends?

    10:30-11:00   Coffee break

    11:00-11:30   Peter Sewell (University of Cambridge)
	              Title: C?
    11:30-12:00   Roderick Chapman (Protean Code Limited), Stuart Matthews (Altran UK) 
                      Title: Are we there yet? 20 years of industrial theorem proving with SPARK
    12:00-12:30   Discussion

    12:30-13:30   Lunch

    13:30-14:00   Giles Reger (University of Manchester), 
	              Title: Cooperating Proof Attempts in Vampire
	              [RI Project] REVES: REasoning in VErification and Security 
				  
    14:00-14:30   Azeim Chawdhary and Ed Robbins (University of Kent),
	              Title: Type recovery and decompilation are a marriage made in heaven 
	              [RI Projects] SeMaMatch: Semantic Malware Matching, 
				    Compositional Security Analysis for Binaries
				  
    14:30-15:00   Chris Novakovic (Imperial College London), 
	              Title: BrowserAudit: Automated Testing of Browser Security Features  
	              [RI Project] Certified Verification of Client-Side Web Programs
    
    15:00-15:30  Tea break and End of Workshop

There is no charge for the workshop, however registration is required. Complimentary tea, coffee, lunches and a workshop dinner will be provided, but participants are expected to make their own travel and accommodation arrangements. Please refer to your invitation email for registration link for attendance and dinner.

Prizes to support PhD students attending FMATS4: The FMATS4 organisers have a limited number of £200 prizes to support PhD students attending the workshop. As there are limited spaces, the prizes will be awarded on a first-come first-served basis and at the discretion of organisers. All prize winners are expected to be present on both workshop days and give a short oral presentation. Prize winners who are in their second or later years of research are encouraged to prepare a poster on their research for display during the workshop.