Collaborative Research: CI-SUSTAIN: StarExec: Cross-Community Infrastructure for Logic Solving

StarExec是一项网络访问计算服务，作为社区资源/基础设施开发(根据先前的NSF拨款)，以支持自动定理证明领域和其他依赖逻辑求解方法的研究领域的研究人员。这些领域的研究小组无法支持他们自己的基础设施，因为硬件成本很高，以及运行和优化大规模求解器执行所需的高度专业知识。StarExec用户可以将求解器和基准程序上传到系统，配置和执行作业以在选定的基准程序上运行选定的求解器，并通过共享数据和构件进行协作。该基础设施最初是为了促进求解器竞赛而开发的，现在在使用逻辑求解器的许多研究领域支持大量用户。随着逻辑解算器的使用扩展到新的研究领域和更大规模的问题，这笔新的拨款通过在爱荷华大学提供额外的硬件(计算集群)和人力资源来支持和扩展StarExec，以满足对这一基础设施日益增长的需求。长期可持续发展战略的一部分是创建多个StarExec软件实例，首先是迈阿密大学，它将作为未来扩张的示范和样板。

StarExec is a web-accessed compute service that was developed (under a prior NSF grant) as a community resource/infrastructure to support researchers in the field of automatic theorem proving and other research areas that depend on logic-solving methods. Research groups in these areas cannot support their own infrastructure due to the high cost of the hardware and the high degree of specialized expertise needed to run and optimize large-scale solver executions. StarExec users can upload solvers and benchmarks to the system, configure and execute jobs to run selected solvers on selected benchmarks, and collaborate by sharing data and artifacts. The infrastructure was first developed to facilitate solver competitions and now supports a large number of users in many areas of research where logic solvers are used. This new grant sustains and expands StarExec by providing additional hardware (computing clusters) and human resources at the University of Iowa to meet the growing demand for this infrastructure, as the use of logic solvers expands to new research areas and larger-scale problems. Part of the long-term, sustainability strategy is to create multiple instances of the StarExec software, starting with the University of Miami, which will serve as a demonstration and model for future expansion.