Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: The L4.verified Project</h1> <div class='date'><time class="dtstart dt-start" title="2010-05-24T10:30:00" datetime="2010-05-24T10:30:00">Monday, May 24, 2010 from 10:30</time>–<time class="dtend dt-end" title="2010-05-24T11:30:00" datetime="2010-05-24T11:30:00">11:30am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>The L4.verified Project Presented by Dr. Gerwin Klein.</p> <p>Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://www.galois.com/blog/2010/05/21/tech-talk-the-l4-verified-project/">Website</a></li> </ul> </div>