University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > From Separation Logic to Systems Code

From Separation Logic to Systems Code

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

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 Computer Laboratory Wednesday Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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