Background

Ongoing breakthroughs in several nationally important research areas depend on continuing advances in high-performance automated theorem proving tools. Important examples include program verification and analysis, combinatorial design, hardware certification, computer security, planning
and artificial intelligence, and the proposed semantic web.

The typical use of these tools is as backends: application problems are translated by an application tool into (often very large or complex) logic formulas, which are then handed off to a logic solver. Over the years, distinct solver communities have grown up around different logics. While these communities have achieved impressive results, specialization has resulted in some barriers between communities, including limited mutual access to artifacts like solvers and benchmarks, and a corresponding limit on exchanges of ideas between communities. Many communities have independently built their own research and development infrastructures, including standard formats for logic formulas, libraries of benchmark formulas, and regular solver
competitions or solver-execution services, to spur solver advances and compare solvers. This independent duplication of equipment and human effort across logic-solving communities is wasteful, and poses a significant barrier to entry for newly developing subfields.

A shared computing infrastructure for logic solving would eliminate wasted effort, reduce the entry barrier for new logic-solver communities, provide a better infrastructure than can be acquired by the individual communities, and promote inter-community activities. The development of a shared computing infrastructure for logic solving is the goal of this project.

Goals

This project will develop a single piece of shared computing infrastructure, called StarExec, that can be used by many different logic solver communities. StarExec will:

1. allow each solver community to manage its benchmark library, community membership, and run its solver competition, on a single shared cluster of compute nodes;
2. provide solver execution and comparison services for registered users and the public;
3. provide services that will help connect different logic-solving communities. This will include translators between (compatible) logics, and a proof checking service based on a proof meta-language called LFSC ("Logical Framework with Side Conditions").

StarExec will utilize community-input mechanisms to ensure the service meets the needs of its target communities and individual users.

Domain Knowledge

Here is a simplified breakdown of what StarExec is aiming to provide. There are different communities out there in the computer science world that are interested in solving very specific logic formulas. The communities often specialize in solving logics with specific properties (e.g. SAT, SMT, ATP, etc.) StarExec is a system that will allow researchers to upload these "formulas" (we call benchmarks) and solvers (the programs that solve them) and run them on our cluster.

As developers, we have a simple notion of what solvers and benchmarks are and do not need to concern ourselves much with the details since that what the researcher's job is! Solvers are nothing but programs. Benchmarks are nothing but inputs to the program. We give a solver a benchmark and we get an answer back. It's as simple as that.

Where the interesting part of designing this seemingly simple system is scale. Each community has benchmark libraries which can be in the hundreds of thousands. It may also take a solver seconds, weeks, days or months to complete one benchmark. Running just 5 solvers on 100,000 benchmarks requires enormous computational power! Also the "answer" we get back from each solver could be as complex as a machine generated proof that could be gigabytes in size. These are all problems the system must deal with.