Proving that Programs Eventually do Something Good
Failures can be sorted into two groups: those that cause the software to do something wrong, and those that result in the software not doing something useful
- Starts at
TU Wien, Campus Karlsplatz
1040 Vienna, Karlsplatz 13
Stiege 1, 1. Stock, AA0148
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 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.
- Dr. Byron Cook, Microsoft Research
Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!