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

摘要计划：NSF 04-588简明计算研究基础设施标题：CRI：协作研究：SMT-LIB，可满足性模理论的公共库和基础设施主导提案：CNS-0551646PI：Tinelli，CesareInstitution：爱荷华大学Proposal：CNS-0551697PI：Stump，Aaron D.Institution：华盛顿大学Proposal：CNS-0551645PI：Barrett，Clark Institution：纽约大学在爱荷华大学、华盛顿大学和纽约大学的研究人员将为可满足性模理论求解器(SMT)的用户和开发者开发社区资源。求解器是用于软件和硬件验证的逻辑推理程序。该项目将制定标准和接口，以便将求解器纳入核查工具和基准，并开发服务，以便对SMT求解器进行准确评价和比较。这些将支持广大研究人员的使用。该项目的更广泛影响是提高了核查方面的研究能力。更长远的好处将包括未来更可靠的硬件和软件系统。

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.