University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Proving that programs eventually do something good

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Proving that programs eventually do something good

Download to your calendar using vCal

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 lists

The Department of Chemistry, University of Cambridge Lensfield Road, Cambridge Hybrid & Department of Chemistry (Pfizer lecture theatre) West 1, West Hub, JJ Thomson Avenue, Cambridge

Other talks

Talk TBC Title and abstract tba Security Cooperation within Government and between Governments External Seminar - Jenn Brophy TBC Precarity and the economy of makeshifts: A novel argument from the census of England, 1851-1911 "That's History. That's Truth. I Seen It Myself": T'tc~tsa (Wailaki) and the Enslavement of California Native Americans.
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity