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

摘要程序：NSF 04-588 CISE计算研究架构标题：CRI：协作研究：SMT-LIB，可满足性模理论的公共库和基础设施领导提案：CNS-0551646 PI：Tinelli，Cesare机构：爱荷华大学提案：CNS-0551697 PI：Stump，Aaron D.机构：华盛顿大学提案：CNS-0551645 PI：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.