![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Peter O'Hearn - Queen Mary University of London
Wednesday 28 April 2010, 14:15-15:15
From Separation Logic to Systems Code
- đ¤ Speaker: Peter O'Hearn - Queen Mary University of London
- đ Date & Time: Wednesday 28 April 2010, 14:15 - 15:15
- đ Venue: Lecture Theatre 1, Computer Laboratory
Questions? Contact
Mateja Jamnik
Abstract
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.
Series This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Chris Davis' list
- computer science
- 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)
- Martin's interesting talks
- School of Technology
- se393's list
- tcw57âs list
- Trust & Technology Initiative - interesting events
- Wednesday Seminars - Department of Computer Science and Technology
- yk373's list
- yk449
Note: Ex-directory lists are not shown.