Morning of Thursday, 21st September 2017
9:30-10:15 Tea and Coffee
10:15-10:20 Welcome, Philippa Gardner (Imperial College London, Director of VeTSS) and Andy Gordon (Principal Researcher at MSR Cambridge)
10:20-11:00 Peter O’Hearn (Facebook London and UCL): Principles and Practice of Interprocedural Reasoning at Scale.
Peter O’Hearn is a principal engineer at Facebook and leader of the team working on the Facebook Infer verification tool. Together with Reynolds, he is the creator of separation logic, used for analysing C and Java programs.
11:00-11:30 Daniel Kroening (Oxford and DiffBlue): Over and under: automating exploits
11:30-12:00 Tea and Coffee
12:00-12:30 Alastair Donaldson (Imperial College): Industrial-strength analysis and testing tools for multicore programming
Alastair Donaldson has an EPSRC Early Career Fellowship and has won the 2017 BCS Roger Needham (mid-career) Award for computer science and engineering as well as the Best paper award at FSE 2017, with Tyler Sorensen and Hugues Evrard. He is the Co-I on the VeTSS funded project Automated Testing for Web Browsers.
12:30-13:00 Short talks for PhD Students, RAs and industrialists
Afternoon of Thursday, 21st September 2017
14:00-14:30 Neil White (Altran UK)
14:30-15:00 Nathan Chong (ARM): Reasoning about Transactional Memory, Axiomatically. SLIDES
Nathan Chong is a Staff Researcher at Arm in the Security and Correctness Group. He works on specification and verification at the hardware/software boundary, including low-level systems code and architecture. Nathan has a PhD from Imperial College and was overall winner of the EPSRC ICT Pioneers competition in 2014.
15:00-15:30 More short talks for PhD Students, RAs and industrialists
15:30-16:00 Tea and Coffee break
16:00-16:30 Boris Köpf (IMDEA, Madrid), Static Quantification of Timing Side Channels
Boris Köpf is an associate research professor at the IMDEA Software Institute in Madrid, Spain. His research focuses on side-channel attacks (and countermeasures) and privacy-preserving data publishing.
16:30-17:00 Antoine Delignat-Lavaud (Microsoft Research): Deploying cryptographically-verified components for the HTTPS ecosystem
17:00-17:30 Discussion: VeTSS: Analysis and Verification in the Industrial Software Design Process
19:30-22:00 Workshop dinner at Westminster College Hall,
Morning of Friday, 22nd September 2017
09:00-09:30 Tea and Coffee
09:30-10:00 Sylvan Clebsch (Microsoft Research) Coco Framework for enterprise Blockchain networks
Sylvan Clebsch is a principal research software development engineer at Microsoft Research. He will talk about the Coco Framework, to improve performance, confidentiality and governance characteristics of enterprise blockchain networks, which is raising some interesting formal methods challenges.
10:00-10:30 Scott Owens (University of Kent, VeTSS’17): Building Trustworthy Software with CakeML
Scott Owens is part of the the team that has developed the functional programming language, Cake ML, with a proven-correct compiler and runtime system. He is the lead researcher on the VeTSS-funded project Verifying Efficient Libraries in CakeML. Ramana Kumar received this yeat’s ACM John C. Reynolds Doctoral Dissertation Award for his PhD thesis on Cake ML.
10:30-10:45 Greta Yorsh (Queen Mary, VeTSS’17): Unbounded Superoptimization
Greta Yorsh was previously a software engineer at ARM, developing open-source compilation tools, and a researcher at IBM Watson, New York. She is the lead researcher on the VeTSS-funded project Supervectorizer.
10:45-11:15 Tea and Coffee break
11:15-11:45 James Cheney (University of Edinburgh, VeTSS’17): Intersection between databases and programming languages. SLIDES
James Cheney is the recipient of an ERC Consolidator Grant to develop Skye, a programming language bridging theory and practice for scientific data curation. He previously held a Royal Society University Research Fellowship. He is the co-lead on the VeTSS-funded project Mechanising the Metatheory of SQL with Nulls, together with Wilmer Ricciotti.
Johannes Kinder is the lead researcher on the VeTSS-funded project EASTEND, and will talk about the assessment and improvement of the reliability and security of software using automated analysis tools, integrating ideas from programming languages, software engineering and systems security.
12.00-12.15 Conrad Watt (Cambridge): Formalising WebAssembly
Conrad Watt is a PhD student at Cambridge University supervised by Peter Sewell. He is currently focussed on formalising the WebAssembly language and its related artefacts, in particular the SharedArrayBuffer proposal.
12.15-12.30 Simon Foster (York, VeTSS’17): Isabelle/UTP: A Verification Toolbox for Unifying Theories. SLIDES
Simon Foster is a Postdoctoral Research Fellow at the University of York working on the EU H2020 project “INTO-CPS” where he researches formal semantics and theorem proving for cyber-physical systems. He is co-investigator on VeTSS funded project “Mechanised Assume-Guarantee Reasoning for Control Law Diagrams via Circus“, and the main developer of the Isabelle/UTP formal semantics and verification toolbox which is the subject of his talk.
12.30-12.45 Kyndylan Nienhuis (Cambridge): Security proofs of the CHERI ISA in Isabelle
Afternoon of Friday, 22nd September 2017
14.00-14.30 Rod Chapman (Protean Code Ltd.): Sanitising Sensitive Data: How to get it Right(or at least Less Wrong…). SLIDES
Rod Chapman, representing Protean Code Ltd., was formerly a principal engineer with Altran UK. Rod specialises in the design process and technologies used in the development of security-critical and safety-critical systems.
14.30-15.00 David Clark (UCL, former RI2 institute (RIAPAV)): Indexing Operators to Extend the Reach of Symbolic Execution.
David Clark‘s research interests include program flow security, slicing programs and software models, malware detection and classification, software testing and application of information theory to software analysis.
15.00-15.30 Mark Batty (University of Kent, VeTSS’17): Industrial concurrency specification for C/C++ SLIDES
Mark Batty’s research focusses on formal specifications, testing tools and verification techniques for real-world concurrent systems, with an emphasis on established programming language interfaces (e.g. C and C++) and concrete testable artefacts (e.g., weak memory models). He has a Lloyds Register Foundation and RAEng Research Fellowship. In 2015, he won the ACM Sigplan John C. Reynolds Doctoral Dissertation Award and the UK BCS/CPHC Distinguished Dissertation Award.