Speaker: Peter O'Hearn
Time:2009-05-11 ~ 11
Place:Room 105, Bldg 302, SNU


Once upon a time, program logics, such as Hoare's logic, were solely the domain of theorists, used to construct manual proofs of tiny, intricate algorithms. In recent years the area has been reinvigorated by developments in both theory and practice. One such development is Separation Logic -- a member of an "exotic" branch of mathematical logic known as substructural logic -- which has provided a way of attacking the old problem of efficient reasoning about dynamically allocated objects in memory. In this talk I describe how you can go from this seemingly exotic logic to a practical software tool for verifying selected integrity properties of low-level systems programs. Along the way, I will draw in some concepts from artificial intelligence and the philosophy of science that help to significantly boost the level of automation in the tool.


[ List ]