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 RDATE:20111106T020000 TZOFFSETFROM:-0700 TZOFFSETTO:-0800 TZNAME:PST END:STANDARD BEGIN:DAYLIGHT DTSTART:20110313T020000 RDATE:20110313T020000 RDATE:20120311T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT 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. \;\n \;\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. \;\n \;\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. \ ;\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 BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20121009T165835Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121016T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121016T103000 DTSTAMP;VALUE=DATE-TIME:20121009T165835Z LAST-MODIFIED;VALUE=DATE-TIME:20121009T165835Z UID:http://calagator.org/events/1250462942 DESCRIPTION:Presented by Matthew Fernandez. \;\n \;\nIn safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences . Formal verification has the potential to provide high assurance for th is software\, but is regarded as being prohibitively expensive. Although significant advances have been made in this area\, verification of larg er systems still remains impractical. Component-based development has th e potential to lower the cost of system-wide verification\, bringing cor rectness proofs of these large scale systems within reach. This talk wil l discuss my work that aims to provide a component-based development env ironment for building systems with high assurance requirements. By provi ding a formal model of the platform with proven correctness properties t hat hold at the level of an abstract model right down to the implementat ion\, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation. \;\n\n\nTags: galois\ , formal methods\, tech talk\, l4\, OS design\, kernels\n\nImported from : http://calagator.org/events/1250462942 URL:https://corp.galois.com/blog/2012/10/9/tech-talk-towards-a-formally-v erified-component-platform.html SUMMARY:Galois Tech Talk: Towards a Formally Verified Component Platform LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR