From Separation Logic to Systems Code
Duration: 1 hour 19 mins 7 secs
Share this media item:
Embed this media item:
Embed this media item:
About this item
| Description: | http://www.talks.cam.ac.uk/talk/index/23757 |
|---|
| Created: | 2010-06-11 13:26 |
|---|---|
| Collection: | Computer Laboratory Wednesday Seminars |
| Publisher: | University of Cambridge |
| Copyright: | Computer Laboratory |
| Language: | eng (English) |
| 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. |
|---|---|
Available Formats
| Format | Quality | Bitrate | Size | |||
|---|---|---|---|---|---|---|
| MPEG-4 Video | 480x360 | 1.84 Mbits/sec | 1.07 GB | View | Download | |
| WebM | 480x360 | 742.78 kbits/sec | 429.78 MB | View | Download | |
| Flash Video | 480x360 | 807.46 kbits/sec | 468.49 MB | View | Download | |
| Flash Video | 320x240 | 438.6 kbits/sec | 254.48 MB | View | Download | |
| iPod Video | 480x360 | 505.34 kbits/sec | 293.20 MB | View | Download | |
| MP3 | 44100 Hz | 125.01 kbits/sec | 72.32 MB | Listen | Download | |
| Auto * | (Allows browser to choose a format it supports) | |||||