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

协作研究：CI-SUSTAIN：StarExec：用于逻辑解决的跨社区基础设施

• 批准号: 1729603
• 负责人: Aaron Stump
• 金额: $ 55.22万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-09-01 至 2023-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1729603&HistoricalAwards=false
• 关键词: Collaborative; Research; CI; SUSTAIN; 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.

StarExec是一个Web访问的计算服务，是作为社区资源/基础设施开发的（在先前的NSF资助下），以支持自动定理证明领域和其他依赖逻辑求解方法的研究领域的研究人员。 这些领域的研究小组无法支持自己的基础设施，因为硬件成本高，运行和优化大规模求解器执行需要高度的专业知识。StarExec用户可以将求解器和基准测试上传到系统，配置和执行作业以在选定的基准测试上运行选定的求解器，并通过共享数据和工件进行协作。 该基础设施最初是为了促进求解器竞赛而开发的，现在支持许多使用逻辑求解器的研究领域的大量用户。这一新的赠款通过在爱荷华州大学提供额外的硬件（计算集群）和人力资源来维持和扩展StarExec，以满足对这一基础设施不断增长的需求，因为逻辑求解器的使用扩展到新的研究领域和更大规模的问题。 长期可持续发展战略的一部分是创建StarExec软件的多个实例，从迈阿密大学开始，这将成为未来扩展的示范和模型。