LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

Proving that programs eventually do something good

Visit website for this news | Export event in iCalendar format

 Byron Cook
Date
Friday, February 18 2011 at 11:00AM
Place
Amphithéâtre Marie Curie (Bâtiment d'Alembert)
Speaker
Byron Cook (Microsoft Research & Queen Mary, University of London)

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.

Bio: 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. See research.microsoft.com/~bycook/ for more information.


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Jan 22
Tue, Jan 29
Tue, Feb 5
Tue, Feb 19

Past seminars