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.