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 求解器生成的证明可能长达 GB，需要优化的证明检查器。该合作项目正在开发一个经过验证的证明检查器，支持一种称为带有附带条件的爱丁堡逻辑框架（LFSC）的灵活格式。 LFSC 是一种用于描述不同证明系统的元语言，从而提供灵活性。验证技术被应用于证明检查器本身，以验证其优化，方法是用一种名为 Guru 的经过验证的编程语言编写它。 CVC3 求解器还添加了对 LFSC 证明的支持。这项研究将通过证明大大提高求解器结果的可信度，从而提高错误检测的能力。