From Substructural Logic to Systems Code

Peter O'Hearn ( Queen Mary University, London )

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.