|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Proving that programs eventually do something good
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:
Note that ex-directory lists are not shown.
Other listsQualitative Research Forum - Open meetings Measuring National Well-Being – what matters to you? School of Technology
Other talksPhase field models for two-fluid systems Planning for Survival in the Cold War Geometric Mechanics & Symmetry: From Finite to Infinite Dimensions short course - day 5 Real wages and the household: Quantifying the economy of makeshifts of the poor in 18th-century England Winton 2nd Annual Symposium on Materials Discovery Recent Advances in Molecular and Cellular Pathology