From Separation Logic to Systems Code

Add to your list(s) Download to your calendar using vCal

• Peter O'Hearn - Queen Mary University of London
• Wednesday 28 April 2010, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact Mateja Jamnik.

Separation Logic is a member of an “exotic” branch of logic, known as substructural logic. In this talk I describe how you can go from this exotic logic to a software tool for verifying selected integrity properties of low-level systems programs. Along the way, I will also draw in some concepts from artificial intelligence and philosophy of science that significantly boost the level of automation.

This talk is based on joint work with Cristiano Calcagno, Dino Distefano and Hongseok Yang on the Space Invader program analyzer.

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list
• yk373's list

Note that ex-directory lists are not shown.