Moving fast with software verification
Professor Peter O'Hearn, Facebook and University College London, UK
This is a story of transporting ideas from theoretical research in reasoning about programs into the fast-moving engineering culture of Facebook. The context is that I landed at Facebook in September of 2013, when we brought the Infer static analyser with us from the verification startup Monoidics. Infer is based on recent research in program analysis, which applied a relatively recent development in logics of programs, separation logic. Infer is deployed internally, running continuously to verify select properties of every code modification in Facebook’s mobile apps; these include the main Facebook apps for Android and iOS, Facebook Messenger, Instagram, and other apps which are used by over a billion people in total. This talk describes our experience deploying verification technology inside Facebook, some the challenges we faced, lessons learned, and speculates on prospects for broader impact of verification technology.
Professor Philippa Gardner, Imperial College London, UK
Avoiding fatal flaws with formal methods
Professor Fred B. Schneider, Cornell University, USA
Formal methods are once again in vogue as a tool for building software systems that can resist attacks. The approach, however, has disappointed before. What might the future hold? We discuss the reasons for those past failures, and we explore what has changed (as well as what hasn't).
A rigorous approach to consistency in cloud databases
Dr Alexey Gotsman, IMDEA Software Institute, Spain
Modern databases underlying large-scale cloud services guarantee immediate availability and tolerate network failures at the expense of providing only weak data consistency guarantees. Unfortunately, we currently lack sophisticated theory and tools that would help programmers in using such databases correctly despite the effects of weak consistency. I will present our ongoing work that uses formal techniques to study how weak consistency in cloud databases affects the correctness of applications using them. Building on it, we aim to improve the programmability and performance of cloud databases.