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

逻辑解算器是一种软件程序，可以完全自动地解算复杂的逻辑公式。计算机科学的许多领域中的问题，如人工智能、程序分析、安全、硬件验证和网络物理系统，都可以忠实地转化为逻辑公式。然后，这些公式可以由逻辑解算器自动求解。在过去的二十年里，至少出现了十个不同的逻辑解决社区，基于不同的逻辑语言和解决技术。这些社区一直在独立地构建计算基础设施，以帮助开发和评估他们的解算器：基准公式库、集群支持的Web服务、年度比赛等等。这些基础设施还为用户提供了一个重要的访问点，他们可以在一个站点找到所有的求解器，甚至在基础设施集群上运行Solver来测试它们的相对能力。本研究的目标是构建一个名为StarExec的共享计算基础设施，该基础设施将被许多不同的逻辑求解社区使用。StarExec将为现有的逻辑解决社区提供改进的服务，并降低新兴社区的进入门槛。StarExec基础设施将由与中型计算集群接口的定制Web服务组成。这一开源服务将允许多个逻辑求解社区托管基准程序库，运行比较不同求解器的作业，以及主办竞赛。StarExec将利用规模经济来提供比大多数个人逻辑解决社区可行的更复杂的服务。StarExec的一个非常重要的目标不仅是配置不同的逻辑解决社区，而且要团结他们。为此，StarExec团队将制定不同社区逻辑语言的语法和证明语义的正式规范。这将使用被称为LFSC(“附带条件的逻辑框架”)的Ameta语言来完成，该语言是在之前的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 be faithfullytranslated 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 manydifferent 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.