Keynote Address: Reasoning with Big Code
Dr. Dino Distefano
Software Engineer at Facebook and Professor of Software Verification at Queen Mary, University of London
For organisations like Facebook, high quality software is important. However, the pace of change and increasing complexity of modern code makes it difficult to produce error-free software. Available tools are often lacking in helping programmers develop more reliable and secure applications. Formal verification is a technique able to detect software errors statically, before a product is actually shipped. Although this aspect makes this technology very appealing in principle, in practice there have been many difficulties that have hindered the application of software verification in industrial environments. In particular, in an organisation like Facebook where the release cycle is fast compared to more traditional industries, the deployment of formal techniques is highly challenging. In this talk we describe our experience in integrating a verification tool based on static analysis into the software development cycle at Facebook.
About Dr. Dino Distefano
Dr. Dino Distefano is Software Engineer at Facebook and Professor of Software Verification at Queen Mary, University of London. His research interests include logic, static analysis, software verification, and programming languages. In recent years Dino’s research focused on automatic source code verification based on the mathematical theory called Separation Logic. He designed the first separation logic program analyser able to prove complex properties of safety and security in industrial software. Later, Dino introduced bi-abduction, an extension to the notion of abductive inference from philosophy of science. Bi-abduction is the key ingredient that has taken automatic verification of pointer programs from a few thousands to millions of lines of code. In 2009 he co-founded Monoidics Ltd, a high-tech start-up providing automatic software verification to safety critical industries. Monoidics was acquired by Facebook in 2013. Dino is the recipient of the Roger Needham Award 2012 and the Royal Academy of Engineering Silver Medal 2014.Sponsored by
