Talk Title: Moving fast with software verification
Talk Abstract: 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.
Bio: 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 few thousands to millions of lines of code. In 2009 he co-founded Monoidics Ltd, a London-based 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.
Talk title: Developing Verified Software Using Leon
Talk Abstract: We present Leon, a verifier for functional Scala programs annotated with contracts and defined on integers and data structures such as algebraic data types. Contracts in Leon can themselves refer to recursively defined functions. Leon aims to find counterexamples when functions do not meet the specifications, and proofs when they do. Moreover, it can optimize run-time checks by eliminating statically checked parts of contracts and doing memoization. For verification Leon uses an incremental function unfolding algorithm (which could be viewed as k-induction) and SMT solvers. For counterexample finding it uses these techniques and additionally specification-based test generation. Leon can also execute specifications (e.g. functions given only by postconditions), by invoking a constraint solver at run time. To make this process more efficient and predictable, Leon supports deductive synthesis of functions form specifications, both interactively and in an automated mode. Synthesis in Leon is currently based on a custom deductive synthesis framework incorporating, for example, syntax-driven rules, rules supporting synthesis procedures, and a form of counterexample guided synthesis. We have also developed resource bound invariant inference for Leon and used it to check abstract worst-case execution time. Another one of our projects developed a compilation technique for Leon that maps real-valued program specifications into finite-precision code while enforcing the desired end-to-end error bounds. Recent work enables Leon to perform program repair when the program does not meet the specification, using error localization, synthesis guided by the original expression, and counterexample-guided synthesis of expressions similar to a given one. Leon is open source and can also be tried from its web environment at leon.epfl.ch .
Bio: Viktor Kuncak is an associate professor in the EPFL School of Computer and Communication Sciences, where he leads the Laboratory for Automated Reasoning and Analysis (http://lara.epfl.ch). He works in formal methods with emphasis on algorithms and tools, such as Leon (http://leon.epfl.ch). He received a PhD degree from the Massachusetts Institute of Technology (MIT) in 2007. He was a program co-chair of FMCAD 2014 and VMCAI 2012, and led an international COST Action to establish standardized formats for verification and synthesis (Rich Model Toolkit). His invited talks include those at LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. He received an ACM SIGSOFT distinguished paper award for work on automated testing. His work on software synthesis procedures was published in the Communications of the ACM as a Research Highlight article. His recent work on Implicit Programming, funded by a European Research Council (ERC) grant, aims to bridge the gap between human goals and their computational realizations.
Talk title: Complexity tolerance: dealing with faults of our own making
Talk Abstract: As planetary exploration has pushed the boundaries to get more and more science at more and more difficult locations in our solar system, spacecraft designers have had to pull out all of the stops to layer new capabilities on top of traditional spacecraft functions. Due to volume and mass constraints most new capabilities have had to be shoe-horned into the system in ways that are often at odds with traditional functional and physical decomposition. The risk associated with the complexity of over loaded functionality has made mission managers reluctant to put too much faith into autonomous systems. The top priority for autonomy has been to maintain vehicle health and safety. Only in the last decade have attempts to add autonomy to increase scientific return for its own sake have been accepted by mission managers. Before autonomy for mission enhancement becomes widely and routinely accepted, we must learn how to overcome the risks associated with validating complex one-of-a kind systems.
Bio: Rob is currently the Mars Program Engineering manager for JPL’s Mars Exploration Program as well as the Chief Engineer for the LDSD (Low Density Supersonic Decelerator) project to test new technologies for slowing down landers using Mars’ atmosphere. Rob Manning was the Chief Engineer for the Mars Science Laboratory (MSL) Project that successfully landed Curiosity Rover on Mars on August 5, 2012. Rob was responsible for ensuring that the design, the test program and the team, working together, would result in a mission that would work. An Engineering Fellow at JPL, Rob has been designing, testing and operating spacecraft for 33 years. In the 1990′s, Rob was the Mars Pathfinder Chief Engineer where he also led the Entry Descent and Landing (EDL) team. After successfully landing and operating the first airbag lander and rover on another planet, he co-conspired the idea to modify the Pathfinder and Sojourner Rover designs to become the Mars Exploration Rovers (MER), Spirit and Opportunity. On MER he led the rover system engineering team as well as the EDL team. After MER he became the Mars Program Chief Engineer where he helped plan and integrate the various Mars missions like Phoenix and Mars Reconnaissance Orbiter as well as plan for MSL and beyond. As a result of his luck at JPL, Rob has received three NASA medals and is in the Aviation Week Magazine Space Laureate Hall of Fame in the Smithsonian Air and Space Museum. In 2004, SpaceNews magazine named Rob as one of 100 people who made a difference in civil, commercial and military space since 1989. Rob is a graduate of Caltech and Whitman College where he studied math, physics, computer science, and control systems. He makes his home in La Canada with his wife Dominique and their daughter, Caline.