Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Large Scale Monadic Refinement - Tales from L4.verified</h1> <div class='date'><time class="dtstart dt-start" title="2008-08-27T10:30:00" datetime="2008-08-27T10:30:00">Wednesday, August 27, 2008 from 10:30</time>–<time class="dtend dt-end" title="2008-08-27T11:30:00" datetime="2008-08-27T11: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>TOPIC: Large Scale Monadic Refinement - Tales from L4.verified</p> <p>SPEAKER: Thomas Sewell, NICTA</p> <p>DATE: <strong>Wednesday</strong> , August 27th, 10.30am</p> <p>LOCATION: Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon</p> <p>ABSTRACT: Components of operating systems have emerged as an attractive target for formal analysis, thanks to the key importance of operating system correctness in establishing the security of a range of applications. These systems present a number of unique challenges for analysis, including their low level implementation and their detailed view of the system state. This talk will address none of these, instead focusing on the challenges of reasoning about (relatively) large, non-modular, inherently imperative software artefacts.</p> <p>The talk will describe the formalisation of the seL4 microkernel using a state monad with nondeterminism and exceptions, present a refinement and Hoare calculus, and discuss the impact of this chosen approach on the effectiveness of the overall verification effort.</p> <p>BIOGRAPHICAL DETAILS: Thomas Sewell is a software engineer with an interest in pure mathematics. He obtained his BE & BSc from UNSW in 2006, and has been working as a proof engineer for NICTA's L4.verified project for two and a half years.</p> <p>ABOUT THE GALOIS TECH TALKS. Galois (<a href="http://galois.com">http://galois.com</a>) has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities.</p> <p>The talks are open and free. If you're planning to attend, dropping a note to <a href="mailto:dons@galois.com">dons@galois.com</a> is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://groups.google.com/group/pdxfunc/browse_thread/thread/40a178872a66bdb3">Website</a></li> </ul> </div>