© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Abstract for Seminar
Software failures can be sorted into two groups: those that cause the software to do something wrong (e.g. crashing), and those that result in the software not doing something useful (e.g. hanging). In recent years automatic tools have been developed which use mathematical proof techniques to certify that software cannot crash. Based on Alan Turing's proof of the halting problem's undecidablity, many have considered the dream of automatically proving the absence of hangs to be impossible. While not refuting Turing's original result, recent research now makes this dream a reality. This lecture will describe this recent work and its application to industrial software.
Dr. Byron Cook is a Principal Researcher at Microsoft Research in Cambridge, UK as well as Professor of Computer Science at Queen Mary, University of London. He is one of the developers of the Terminator program termination proving tool, as well as the SLAM software model checker. See https://research.microsoft.com/en-us/people/bycook/ for more information.