Proving that programs eventually do something good

Add to your list(s) Download to your calendar using vCal

• Byron Cook, Microsoft Research Cambridge
• Tuesday 03 July 2012, 16:45-17:45
• Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge University Engineering Department Talks
• Centre for Smart Infrastructure & Construction
• Featured lists
• Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Methodology in design research
• Microsoft Research Cambridge, public talks
• School of Technology
• de239's list
• engineering

Note that ex-directory lists are not shown.