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

摘要项目：NSF 04-588 CISE计算研究基础设施项目：CRI：合作研究：SMT-LIB，一个通用库和可满足模理论基础设施牵头提案：CNS-0551646PI: Tinelli， cesare机构：爱荷华大学提案：CNS-0551697PI: Stump， Aaron d .机构：华盛顿大学提案：CNS-0551645PI: Barrett， clark机构：爱荷华大学、华盛顿大学和纽约大学的研究人员将为可满足模理论（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.