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

逻辑求解器是一种软件程序，可以完全自动地求解复杂的逻辑公式。 在计算机科学的许多领域，如人工智能，程序分析，安全，硬件验证和网络物理系统的问题可以被转换成逻辑公式。 这些公式可以由逻辑求解器自动求解。在过去的二十年里，至少有十个不同的逻辑解决社区已经出现，基于不同的逻辑语言和解决技术。 这些社区一直在独立地构建计算基础设施，以帮助开发和评估其求解器：基准公式库、集群支持的网络服务、年度竞赛等等。这样的基础设施还为用户提供了一个重要的访问点，用户可以在一个站点找到所有的求解器，或者甚至在基础设施集群上运行solverson来测试它们的相对能力。本研究的目标是构建一个单一的共享计算基础设施称为StarExec，它将被不同的逻辑解决社区使用。 StarExec将为已建立的逻辑解决社区提供改进的服务，并降低新的和新兴社区的进入门槛。StarExec基础设施将包括一个与中型计算集群接口的自定义Web服务。 这种开源服务将允许多个逻辑求解社区托管基准库，运行比较不同求解器的作业，并举办竞赛。 StarExec将利用规模经济来提供比大多数个人逻辑解决社区更复杂的服务。 StarExec的一个非常重要的目标不仅仅是配置不同的逻辑解决社区，而是将它们联合起来。 为此，StarExec团队将开发不同社区逻辑语言的语法和证明理论语义的正式规范。 这将使用称为LFSC（“附带条件的逻辑框架”）的元语言来完成，该语言是在以前的NSF资助的研究中开发的。 将实现不同逻辑的兼容片段之间的公式翻译，这将使求解器社区之间的集成程度比以前更高。 例如，一个社区中的求解器可以在另一个社区的基准上运行。 这种集成也将帮助逻辑求解器的用户，他们将有更多的选择，所有在一个共同的框架，以解决他们的问题。 StarExec项目更广泛的影响是加速不同逻辑解决技术的开发、采用和融合。 这将使国家重要的应用领域取得更快的进展，如人工智能，验证，安全和网络物理系统，这些领域越来越依赖于高性能逻辑求解器。

Logic solvers are software programs that can solve complex logicalformulas fully automatically. Problems in many areas of ComputerScience, such as artificial intelligence, program analysis, security,hardware verification, and cyber-physical systems can betranslated into logical formulas. Those formulas can then be solvedfully automatically by logic solvers. Over the past two decades, atleast ten different logic-solving communities have emerged, based ondifferent logical languages and solving techniques. These communitieshave independently been building computing infrastructure to aiddevelopment and evaluation of their solvers: libraries of benchmarkformulas, cluster-backed web services, annual competitions, and more.Such infrastructure also provides an important access point forusers, who can find all the solvers at one site, or even run solverson the infrastructure cluster to test their relative capabilities.The goal of this research is to build a single piece of sharedcomputing infrastructure called StarExec, which will be used by different logic solving communities. StarExec will provide improvedservices for established logic-solving communities, and lower theentry barrier for new and emerging communities.The StarExec infrastructure will consist of a custom web serviceinterfacing to a medium-sized compute cluster. This open-sourceservice will allow multiple logic-solving communities to hostbenchmark libraries, run jobs comparing different solvers, and hostcompetitions. StarExec will leverage economies of scale to providemore sophisticated services than is feasible for most individuallogic-solving communities. A very important goal of StarExec is notjust to collocate different logic-solving communities, but to unitethem. To this end, the StarExec team will develop formalspecifications of both the syntax and proof-theoretic semantics ofdifferent communities' logical languages. This will be done using ameta-language called LFSC ("Logical Framework with Side Conditions"),developed in previous NSF-funded research. Translation of formulasbetween compatible fragments of different logics will be implemented,which will will enable a greater degree of integration between solvercommunities than was previously possible. For example, it will bepossible for solvers in one community to be run on benchmarks fromanother. This integration will also aid users of logic solvers, whowill have a greater variety of options, all in a common framework, forsolving their problems. The broader impact of the StarExec projectwill be to accelerate the development, adoption, and convergence ofdifferent logic-solving technologies. This will enable fasterprogress in nationally important application areas such as artificialintelligence, verification, security, and cyber-physical systems,which increasingly depend on high-performance logic solvers.