CRI: Collaborative Research: SMT-LIB, A Common Library and Infrastructure for Satisfiability Modulo Theories

CRI：协作研究：SMT-LIB，可满足性模理论的通用库和基础设施

• 批准号: 0551646
• 负责人: Cesare Tinelli
• 金额: $ 16.09万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-08-01 至 2008-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0551646&HistoricalAwards=false
• 关键词: CRI; Collaborative; Research; SMT; LIB

AbstractProgram: NSF 04-588 CISE Computing Research InfrastructureTitle: CRI: Collaborative Research: SMT-LIB, A Common Library and Infrastructure for Satisfiability Modulo Theories Lead Proposal: CNS-0551646PI: Tinelli, CesareInstitution: University of IowaProposal: CNS-0551697PI: Stump, Aaron D.Institution: Washington UniversityProposal: CNS-0551645PI: Barrett, ClarkInstitution: New York University Investigators at the University of Iowa, Washington University and New York University will develop a community resource for users and developers of solvers for satisfiability modulo theories (SMT). The solvers are logical reasoning programs used in software and hardware verification. The project will develop standards and interfaces to enable incorporation of solvers into verification tools and benchmarks and develop services for accurate evaluation and comparison of SMT solvers. These will support use by a broad community of researchers. Broader impacts of this project are the improvement of research capability in verification. Longer-range benefits will include more reliable future hardware and software systems.

AbstractProgram: NSF 04-588 CISE Computing Research InfrastructureTitle: CRI: Collaborative Research: SMT-LIB, A Common Library and Infrastructure for Satisfiability Modulo Theories Lead Proposal: CNS-0551646PI: Tinelli, CesareInstitution: University of IowaProposal: CNS-0551697PI: Stump, Aaron D.机构：华盛顿大学普罗帕萨尔：CNS-0551645PI：Barrett，Clarkinstitution：爱荷华大学，华盛顿大学和纽约大学的纽约大学调查人员将为Solvers和Solvers的开发人员开发社区资源，以获得满意度模型理论（SMT）。求解器是软件和硬件验证中使用的逻辑推理程序。该项目将开发标准和接口，以使求解器能够将求解器纳入验证工具和基准测试，并开发服务以进行准确的评估和比较SMT求解器。这些将支持广泛的研究人员的使用。该项目的更广泛的影响是提高验证研究能力。较长的好处将包括更可靠的未来硬件和软件系统。