Ongoing breakthroughs in nationally important research areas like Verification and Artificial Intelligence depend on continuing advances in high-performance automated theorem proving tools. The typical use of these tools is as backends: application problems are translated by an application tool into (typically very large and complex) logic formulas, which are then handed off to a logic solver. Different tradeoffs between linguistic expressiveness and the difficulty of solving the resulting problems give rise to different logics. Solver communities, formed around these different logics, have developed their own community research infrastructures to encourage innovation and ease adoption of their solver technology. Such infrastructure includes standard formats for logic formulas, libraries of benchmark formulas, and regular solver competitions to spur solver advances.
Currently, these different infrastructures are all developed separately, at significant cost in equipment and support. These costs are paid again and again for the different services, since there is currently no global piece of computing infrastructure suitable for the logic solving domain, which all these communities can use. This project is building a simplified proof-of-concept of a single piece of shared computing infrastructure, which could eventually be used by many different logic solver communities. The award also provides other support for soliciting research community feedback on the prototype and the design of a comprehensive infrastructure.
Ongoing breakthroughs in internationally important research areas like Verification and Artificial Intelligence depend on continuing advances in high-performance logic-solving tools. These are programs which can automatically prove certain simple but large (tens of megabytes) mathematical/logical statements. Different research communities, on the order of a dozen or so, have developed based around different logics to be solved. The work of this planning grant was a first step towards creating a single piece of shared computing infrastructure, called StarExec, to be used by researchers in different logic-solving communities. Up to now, these communities have each implemented their own infrastructure for testing their solvers and comparing the performance of solvers on large real-world benchmark problems. StarExec will eliminate duplicated efforts by providing a single piece of infrastructure that all these communities can share. Furthermore, by bringing these disparate communities together within a single web-based compute service, StarExec will foster new interactions and collaborations across logic-solving fields. In the course of this planning grant, the PIs designed and implemented a limited prototype of StarExec. This played an important role in applying for a major grant from NSF to develop the fully featured version. As part of the planning work, the PIs organized an international research workshop called "Evaluation Methods for Solvers, Quality Metrics for Solutions" (EMSQMS), in Summer 2010. This workshop was attended by well-known researchers from a variety of logic-solving communities around the world. They provided invaluable feedback in an open forum at EMSQMS on desired features of StarExec, and expressed great enthusiasm for using such a service, if it were funded and built. Based on the work of this planning grant, the full proposal for StarExec has been funded. When completed, StarExec will be an international focus point for the evaluation of logic solvers. The capabilities it will provide will drive further innovation in logic-solving, thus providing the logic-solving power required by advanced applications.
