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

SHF：小型：协作研究：灵活、高效且值得信赖的可满足性模理论证明检查

• 批准号: 0914956
• 负责人: Clark Barrett
• 金额: $ 15万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-08-01 至 2011-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0914956&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Flexible

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.

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。软件漏洞每年给美国经济造成的损失超过600亿美元。 有前途的错误检测技术依赖于可满足性模理论（SMT）的高性能逻辑求解器，它采用复杂的算法来有效地检查大型公式。复杂性是有代价的：求解器本身存在缺陷，对于安全关键型应用程序来说不够可靠。为了增加可信度，一些SMT求解器可以为有效公式发出形式证明。用一个简单的证明检查器检查这些证明，确认求解器的结果。SMT的丰富逻辑为所有SMT求解器的单一证明格式标准化带来了挑战。此外，SMT求解器生成的证明可能长达千兆字节，需要优化的证明检查器。该合作项目正在开发一个经过验证的证明检查器，支持一种名为带附加条件的爱丁堡逻辑框架（LFSC）的灵活格式。LFSC是一种描述不同证明系统的元语言，因此提供了灵活性。验证技术正在应用于证明检查器本身，以验证其优化，方法是用一种名为Guru的验证编程语言编写它。支持LFSC证明也被添加到CVC 3求解器。这项研究将通过证明大大提高求解器结果的可信度，从而提高bug检测的能力。