![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > Automatic termination proofs for software
![]() Automatic termination proofs for softwareAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Timothy G. Griffin. I will describe recent advances in the area of automatic program termination analysis. In particular, I will describe the development of several automatic tools, called TERMINATOR and MUTANT , which implement new termination analysis algorithms. These tools have been used to prove that Windows device driver dispatch routines always return control back to their caller. The tools have also found a number of critical termination bugs in device drivers. Bio: Dr. Byron Cook is a researcher at Microsoft Research, Cambridge. His research interests include automatic formal software verification, automatic theorem proving, and programming language theory. Before coming to Cambridge Byron co-developed the SLAM software model checker. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers. Before joining Microsoft, Byron worked at Prover Technology. Byron’s PhD is from OGI . For more information about Byron, see http://research.microsoft.com/~bycook. This talk is part of the Computer Laboratory Wednesday Seminars series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsEducation Society Cambridge (ESC) National Biology Week talks Babbage Seminar SeriesOther talksThe role of the oculomotor system in visual attention and visual short-term memory Enhanced Decision Making in Drug Discovery Pruning and grafting syntactic trees for cross-lingual transfer tasks Reserved for CambPlants Foster Talk - CANCELLED - Redox Oscillations in the Circadian Clockwork Participatory approaches to encourage responsible use of antibiotics in livestock Computing High Resolution Health(care) Statistical Methods in Pre- and Clinical Drug Development: Tumour Growth-Inhibition Model Example ***PLEASE NOTE THIS SEMINAR IS CANCELLED*** 'Cryptocurrency and BLOCKCHAIN – PAST, PRESENT AND FUTURE' "Mechanosensitive regulation of cancer epigenetics and pluripotency" Systems for Big Data Applications:Revolutionising personal computing |