Logic solvers are software programs that can solve complex logical formulas fully automatically. Problems in many areas of Computer Science, such as artificial intelligence, program analysis, security, hardware verification, and cyber-physical systems can be translated into logical formulas. Those formulas can then be solved fully automatically by logic solvers. Over the past two decades, at least ten different logic-solving communities have emerged, based on different logical languages and solving techniques. These communities have independently been building computing infrastructure to aid development and evaluation of their solvers: libraries of benchmark formulas, cluster-backed web services, annual competitions, and more. Such infrastructure also provides an important access point for users, who can find all the solvers at one site, or even run solvers on the infrastructure cluster to test their relative capabilities.
The goal of this research is to build a single piece of shared computing infrastructure called StarExec, which will be used by different logic solving communities. StarExec will provide improved services for established logic-solving communities, and lower the entry barrier for new and emerging communities.
The StarExec infrastructure will consist of a custom web service interfacing to a medium-sized compute cluster. This open-source service will allow multiple logic-solving communities to host benchmark libraries, run jobs comparing different solvers, and host competitions. StarExec will leverage economies of scale to provide more sophisticated services than is feasible for most individual logic-solving communities. A very important goal of StarExec is not just to collocate different logic-solving communities, but to unite them. To this end, the StarExec team will develop formal specifications of both the syntax and proof-theoretic semantics of different communities' logical languages. This will be done using a meta-language called LFSC ("Logical Framework with Side Conditions"), developed in previous NSF-funded research. Translation of formulas between compatible fragments of different logics will be implemented, which will will enable a greater degree of integration between solver communities than was previously possible. For example, it will be possible for solvers in one community to be run on benchmarks from another. This integration will also aid users of logic solvers, who will have a greater variety of options, all in a common framework, for solving their problems. The broader impact of the StarExec project will be to accelerate the development, adoption, and convergence of different logic-solving technologies. This will enable faster progress in nationally important application areas such as artificial intelligence, verification, security, and cyber-physical systems, which increasingly depend on high-performance logic solvers.
