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

University Of Iowa, Iowa City IA

Investigators

Abstract

Abstract Program: NSF 04-588 CISE Computing Research Infrastructure Title: CRI: Collaborative Research: SMT-LIB, A Common Library and Infrastructure for Satisfiability Modulo Theories Lead Proposal: CNS-0551646 PI: Tinelli, Cesare Institution: University of Iowa Proposal: CNS-0551697 PI: Stump, Aaron D. Institution: Washington University Proposal: CNS-0551645 PI: Barrett, Clark Institution: 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.