Research Scientist Dr. Andrew Reynolds was recently awarded an NSF Grant entitled "Efficient SMT Procedures for Scalable Synthesis in Software Development." The project will develop new functionality in Satisfiability Modulo Theories (SMT) solvers to meet the needs of emerging synthesis problems in several domains. This includes new procedures for solving constraints in known logical fragments of interest such as fixed-width bit-vector formulas with one quantifier alternation, as well as new fragments such as unbounded strings and regular expressions where existing support in SMT solvers is limited. We expect the project to both contribute to the state-of-the-art in SMT solving, and to benefit other reasoning tools such as higher-order theorem provers and model-checkers that rely on invariant synthesis.
This two-year project has been awarded $174,907.