SHF: Small:Collaborative Research: Flexible, Efficient, and Trustworthy Proof Checking for Satisfiability Modulo Theories

点击翻译按钮获取中文摘要

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).Software bugs cost the U.S. economy over $60 billion each year. Promising bug-detection technology depends on high-performance logic solvers for Satisfiability Modulo Theories (SMT), which employ sophisticated algorithms to check large formulas efficiently. Sophistication has a price: the solvers themselves exhibit bugs, and are not trustworthy enough for safety-critical applications. To increase confidence, some SMT solvers can emit formal proofs for valid formulas. Checking these proofs with a simple proof checker confirms the solver's results. SMT's rich logic poses challenges for standardizing a single proof format for all SMT solvers. Furthermore, proofs produced by SMT solvers can be gigabytes long, requiring an optimized proof checker. This collaborative project is developing a verified proof checker supporting a flexible format called the Edinburgh Logical Framework with Side Conditions (LFSC). LFSC is a meta-language for describing different proof systems, thus providing flexibility. Verification techniques are being applied to the proof checker itself to verify its optimizations, by writing it in a verified programming language called Guru. Support is also being added for LFSC proofs to the CVC3 solver. This research will greatly increase confidence in solver results through proofs, thus increasing the power of bug detection.