BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:STANDARD
DTSTART:20101107T020000
RDATE:20101107T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110126T230643Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110201T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110201T103000
DTSTAMP;VALUE=DATE-TIME:20110126T230643Z
LAST-MODIFIED;VALUE=DATE-TIME:20110126T230643Z
UID:http://calagator.org/events/1250459683
DESCRIPTION:Presented by Simon Winwood.&#13\;\n&#13\;\nIn 2009 the NICTA 
 L4.verified project completed the machine-checked correctness proof of t
 he seL4 microkernel. The natural next step is then to use this verified 
 kernel to construct verified systems.&#13\;\n&#13\;\nIn this talk I give
  an overview of the ongoing work into systems verification in the Trustw
 orthy Embedded Systems project. In particular\, I will focus on the use 
 of access control results to reason about the properties of systems in t
 he presence of large untrusted components\, such as a Linux kernel.&#13\
 ;\n\n\nTags: galois\, tech talk\, l4\, os\n\nImported from: http://calag
 ator.org/events/1250459683
URL:http://corp.galois.com/blog/2011/1/26/tech-talk-verifying-sel4-based-
 systems.html
SUMMARY:Galois Tech talk: Verifying seL4-based Systems
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR