Chairs
Professor Gordon Plotkin
Professor Gordon Plotkin
After an undergraduate degree in Mathematics and Physics, obtained from Glasgow University, Gordon Plotkin obtained a doctorate in Artificial Intelligence from Edinburgh University in 1972. He then joined the faculty at Edinburgh, becoming a full professor in 1986. He is a Fellow of the Royal Society, a Fellow of the Royal Society of Edinburgh, and a member of Academia Europaea. He may be best known for his work on the operational semantics of programming languages, in particular for Structural Operational Semantics. He has also contributed to many other areas of the semantics and logic of programming languages, and, more recently, to simulation languages for systems biology. His prizes include the ACM Programming Languages Achievement Award and the Royal Society Milner Award.
09:00-09:35
Moving fast with software verification
Professor Peter O'Hearn, Facebook and University College London, UK
Abstract
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.
Show speakers
Professor Peter O'Hearn, Facebook and University College London, UK
Professor Peter O'Hearn, Facebook and University College London, UK
Peter O’Hearn works as an Engineering Manager at Facebook with the Static Analysis Tools team, and as a Professor of Computer Science at University College London. Peter held academic positions at Syracuse and Queen Mary before UCL, and is the past recipient of a Royal Society Wolfson Research Merit Award, a Most Influential POPL Paper Award, and a Royal Academy of Engineering/Microsoft Research Chair.
His research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of program proof. With John Reynolds he developed separation logic, a theory which opened up new practical possibilities for program proof. In 2009 he cofounded a software verification start-up company, Monoidics Ltd, which was acquired by Facebook in 2013. The Facebook Infer program analyser, recently open-sourced, runs on every modification to the code of Facebook’s mobile apps, in a typical month issuing millions of calls to a custom separation logic theorem prover and resulting in hundreds of bugs being fixed before they reach production.
09:35-10:10
Understanding and verifying JavaScript programs
Professor Philippa Gardner, Imperial College London, UK
Abstract
JavaScript is the most widely used language for client-side web applications. The dynamic nature of JavaScript, together with its complicated semantics, makes the understanding and development of JavaScript code notoriously difficult. Because of this, JavaScript programmers still have very little tool support for catching errors early in development, compared with the abundance of tools (such as IDEs and specialised static analysis tools) that are available for more traditional languages such as C and Java.
The development of such analysis tools for JavaScript web applications is known to be a challenging task. In this talk, I will describe:
--JSCert, a Coq mechanised specification of JavaScript which is line-by-line close to the English standard. It has an accompanying reference interpreter, which is provably correct with respect to JSCert and tested using the official test suite.
--JSIL, an intermediate language for JavaScript with a semantics-driven compiler which has been proved correct for a significant fragment and properly tested. In future, we will develop JSIL front-ends for verification tools based on symbolic execution, such as CBMC used by Amazon, Infer developed at Facebook and Rosette.
--JSVerify, a fledgling symbolic execution tool which has currently been used to verify JSIL implementations of the internal and built-in functions of JavaScript. In future, we will develop a substantial JavaScript verification tool, requiring a formal link between the JavaScript and JSIL program logics, a large engineering effort to make the verification tractable, and the verification of substantial program examples such as those from Google’s V8 array library.
Our ultimate goal is to develop a trusted service for understanding and verifying JavaScript programs.
Show speakers
Professor Philippa Gardner, Imperial College London, UK
Professor Philippa Gardner, Imperial College London, UK
Philippa Gardner is a professor in the Department of Computing at Imperial. Her current research focusses on program verification: in particular, reasoning about web programs (JavaScript and DOM) and reasoning about concurrent programs. She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh, in 1992. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial. She is the Director of the Research Institute in Automated Program Analysis and Verification, funded by GCHQ in association with EPSRC.
10:40-11:15
Avoiding fatal flaws with formal methods
Professor Fred B. Schneider, Cornell University, USA
Abstract
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).
Show speakers
Professor Fred B. Schneider, Cornell University, USA
Professor Fred B. Schneider, Cornell University, USA
Fred B. Schneider is Samuel B. Eckert Professor of Computer Science at Cornell University and chair of the department. Schneider's research has focused on various aspects of trustworthy systems -systems that will perform as expected, despite failures and attacks. Schneider was named Professor-at-Large at the University of Tromso (Norway) in 1996 and was awarded a Doctor of Science honoris causa by the University of Newcastle-upon-Tyne in 2003 for his work in computer dependability and security. He received the 2012 IEEE Emanuel R. Piore Award for ‘contributions to trustworthy computing through novel approaches to security, fault-tolerance and formal methods for concurrent and distributed systems’. The U.S. National Academy of Engineering elected Schneider to membership in 2011, and the Norges Tekniske Vitenskapsakademi (Norwegian Academy of Technological Sciences) named him a foreign member in 2010.
11:15-11:50
A rigorous approach to consistency in cloud databases
Dr Alexey Gotsman, IMDEA Software Institute, Spain
Abstract
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.
Show speakers
Dr Alexey Gotsman, IMDEA Software Institute, Spain
Dr Alexey Gotsman, IMDEA Software Institute, Spain
Alexey Gotsman is an Assistant Research Professor at the IMDEA Software Institute in Madrid, Spain. Before joining IMDEA, he was a postdoctoral fellow at the University of Cambridge, where he also got his Ph.D. Alexey's research interests are in programming models and verification techniques for concurrent and distributed software.