Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Duckki Oe, Formally Certified Satisfiability Solving</h1> <div class='date'><time class="dtstart dt-start" title="2012-04-13T13:30:00" datetime="2012-04-13T13:30:00">Friday, April 13, 2012 from 1:30</time>–<time class="dtend dt-end" title="2012-04-13T14:30:00" datetime="2012-04-13T14:30:00">2:30pm</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202391953'><span class='fn org p-name'>Portland State University FAB, Room 86-09</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">1900 SW Fourth Avenue</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">Oregon</span> <span class="postal-code p-postal-code">97201</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=1900%20SW%20Fourth%20Avenue,%20Portland%20Oregon%2097201%20US'>map</a>) </div> </div> <div class="description p-description"> <p>Abstract:</p> <p>Satisfiability (SAT) and satisfiability module theories (SMT) solvers are efficient automated theorem provers widely used in several fields such as formal verification and artificial intelligence. Although SAT/SMT are traditional propositional and predicate logics and well understood, SAT/SMT solvers are complex software highly optimized for performance. Because SAT/SMT solvers are commonly used as the final verdict for formal verification problems, their correctness is an important issue. This talk discusses two methods to formally certify SAT/SMT solvers. First method is generating proofs from solvers and certifying those proofs. One of the issues for proof checking is that SMT logics are constantly growing and a flexible framework to express proof rules is needed. The proposal is to use a meta-language called LFSC, which is based on Edinburgh Logical Frame with an extension for expressing computational side conditions. SAT and SMT logics can be encoded in LFSC, and the encoding can be easily and safely extended for new logics. And it has been shown that an optimized LFSC checker can certify SMT proofs very efficiently. Second method is using a verified programming language to implement a SAT solver and verify the code statically. Guru is a pure functional programming language with support for dependent types and theorem proving. A modern SAT solver has been implemented and verified to be correct in Guru. Also, Guru allows very efficient code generation through resource types, so the performance of versat is comparable with that of the current proof checking technology with a state-of-the-art solver.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://www.pdx.edu/computer-science/colloquium-and-other-events-0">Website</a></li> </ul> </div>