ROSAEC center Seoul National University
NRF

Seminars & Workshops

Speaker:Duckki Oe , ComputationaLogic Center
When:2012-04-23 15:00
Place:Room 309, Bldg 302, SNU

Abstract

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, therefore 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 with low-level optimizations. 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.

Short bio

2008--present Ph.D candidate, University of Iowa 2008 Master's in Computer Science, Washington University in St. Louis 2006 Bachelor in Computer Science, Yonsei University

Resources



© Copyright 2008-2010 ROSAEC Center, Seoul National University