BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:CN: A separation-logic refinement type system for production syste
 ms code verification - Neel Krishnaswami (University of Cambridge)
DTSTART:20220708T150000Z
DTEND:20220708T160000Z
UID:TALK175802@talks.cam.ac.uk
DESCRIPTION:CN is a type system for C code\, aimed at verifying the safety
  and functional correctness of systems C code (i.e.\, the kind found in ke
 rnels and hypervisors).\nVerification of C code is by no means a novel obj
 ective\, but the aim of CN is to yield a developer experience that is much
  more like using a conventional type checker (albeit one with rich types) 
 than using a full-fledged proof assistant. The goal (not achieved yet!) is
  for CN to process moderately-annotated source code and to reliably\, pred
 ictably\, and reasonably quickly return either a confirmation that the cod
 e satisfies the specifications\, or an error message that gives useful fee
 dback as to why not. This contrasts with the experience of using a proof a
 ssistant like Coq\, which deliberately sacrifices reliability and predicta
 bility in order to permit users to write heuristics and tactics to do proo
 f search.&nbsp\;\nIn our talk\, we will discuss the design and implementat
 ion of the CN type system\, demonstrating some of the tooling we havebuilt
  (based on the Visual Studio Code Language Server Protocol)\, by showing w
 hat CN code looks like when we are writing specifications for (part of) th
 e pKVM hypervisor which is intended to underlie Android in the future. Thi
 s will show both the strengths (CN works on actual C systems code we didn'
 t write ourselves!) and the weaknesses of our approach (C idioms which are
  hard to capture with our approach\, such as offset calculations involving
  nonlinear arithmetic).\n&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR