BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Wrestling with real systems - Peter Sewell (University of Cambridg
 e)
DTSTART:20220707T123000Z
DTEND:20220707T133000Z
UID:TALK175781@talks.cam.ac.uk
DESCRIPTION:Systems software is often security critical\, so a tempting ta
 rget for verification\, but verification needs a trustworthy semantics for
  the underlying architecture\, and verification techniques that can handle
  it. Neither exist yet\, for any major production architecture\, so previo
 us work has had to idealise\, simplify\, or pretend - but we're getting cl
 oser. &nbsp\;In this talk I'll describe recent and ongoing work to establi
 sh the pieces of this challenging jigsaw\, and start fitting them together
  and using them\, focussing especially on Morello (capability-enabled CHER
 I-Arm) sequential semantics and security proofs\, and on Arm-A sequential 
 and relaxed virtual-memory concurrent semantics and reasoning. I'll mentio
 n some pros and cons of wrestling with real-world architecture.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR