BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium : Moving fast with software verification
DTSTART:20151130T161500
DTEND:20151130T173000
DTSTAMP:20260407T175843Z
UID:1c39887841ef851594dbaae9af68eb529cb530acb7a8143bf846ad42
CATEGORIES:Conferences - Seminars
DESCRIPTION:By : Dino Distefano - Queen Mary\, University of LondonAbstrac
 t :\nFor organisations like Facebook\, high quality software is important.
  However\, the pace of change and increasing complexity of modern code mak
 es it difficult to produce error-free software. Available tools are often 
 lacking in helping programmers develop more reliable and secure applicatio
 ns. Formal verification is a technique able to detect software errors stat
 ically\, 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 verificat
 ion in industrial environments. In particular\, in an organisation like Fa
 cebook where the release cycle is fast compared to more traditional indust
 ries\, the deployment of formal techniques is highly challenging. In this 
 talk we describe our experience in integrating a verification tool based o
 n static analysis into the software development cycle at Facebook.Bio :\nD
 r. Dino Distefano is Software Engineer at Facebook and Professor of Softwa
 re Verification at Queen Mary\, University of London. His research interes
 ts include logic\, static analysis\, software verification\, and programmi
 ng languages. In recent years Dino’s research focused on automatic sourc
 e code verification based on the mathematical theory called Separation Log
 ic. 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 inf
 erence from philosophy of science. Bi-abduction is the key ingredient that
  has taken automatic verification of pointer programs from few thousands t
 o millions of lines of code. In 2009 he co-founded Monoidics Ltd\, a Londo
 n-based high-tech start-up providing automatic software verification to sa
 fety 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.More information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR