![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Byron Cook - Microsoft Research Cambridge
Wednesday 17 February 2010, 14:15-15:15
Proving that programs eventually do something good
- đ¤ Speaker: Byron Cook - Microsoft Research Cambridge
- đ Date & Time: Wednesday 17 February 2010, 14:15 - 15:15
- đ Venue: Lecture Theatre 1, Computer Laboratory
Abstract
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.
Series This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Chris Davis' list
- computer science
- Department of Computer Science and Technology talks and seminars
- Graduate-Seminars
- Guy Emerson's list
- Interested Talks
- Lecture Theatre 1, Computer Laboratory
- Martin's interesting talks
- School of Technology
- se393's list
- Trust & Technology Initiative - interesting events
- Wednesday Seminars - Department of Computer Science and Technology
- yk449
Note: Ex-directory lists are not shown.