Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


From Substructural Logic to Systems Code

  • Speaker:   Professor  Peter O'Hearn  (University of London)
  • Host:   Richard Banach
  • 18th February 2009 at 14:15 in Lecture Theatre 1.4, Kilburn Building
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 certain integrity properties of low-level systems programs. I will introduce Separation Logic via its model theory, and the explain how proof theory is the conduit through which its ideas can flow into a program analyzer. 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.
▲ Up to the top