ICE: Learning Correctness Proofs of Software

28^th January 2020, 13:00 Ashton Lecture Theater
Dr. Daniel Neider
Max Planck Institute for Software Systems
University of Kaiserslautern

Abstract

Software systems have become ubiquitous in our modern world and, consequently, so have bugs and glitches. While many software failures are harmless and often merely annoying, some can have catastrophic consequences. Just imagine the dire results of an autonomous car failing to stop at a red traffic light or a plane's control system becoming
unresponsive during takeoff or landing.

In this talk, I will present ICE, a technique for formally proving the correctness of software. ICE combines inductive techniques from the area of machine learning with deductive techniques from the area of logic to infer correctness proofs of programs in a fully automated manner. Moreover, I will briefly survey various other application areas where
the ideas underlying ICE have been applied, such as the synthesis of reactive controllers.