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

点击翻译按钮获取中文摘要

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.