Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
PhD: Proving that programs eventually do something good

Speaker  Byron Cook

Affiliation  MSR Cambridge


Duration  00:59:22

Date recorded  3 July 2012

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. But, based on Alan Turing's proof of the halting problem's undecidability, 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.

©2012 Microsoft Corporation. All rights reserved.
By the same speaker
> PhD: Proving that programs eventually do something good