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

逻辑求解器是能够完全自动地求解复杂逻辑公式的软件程序。计算机科学许多领域的问题，如人工智能、程序分析、安全、硬件验证和网络物理系统，都可以忠实地转化为逻辑公式。然后，这些公式可以由逻辑求解器自动求解。在过去的二十年里，至少出现了十个不同的逻辑求解社区，它们基于不同的逻辑语言和求解技术。这些社区已经独立地构建了计算基础设施，以帮助开发和评估他们的解决方案：基准公式库、集群支持的web服务、年度竞赛等等。这种基础设施还为用户提供了一个重要的访问点，用户可以在一个站点上找到所有的求解器，甚至可以在基础设施集群中运行求解器来测试它们的相关功能。这项研究的目标是建立一个称为starrexec的共享计算基础设施，它将被许多不同的逻辑解决社区使用。starrexec将为已建立的逻辑解决社区提供改进的服务，并降低新社区和新兴社区的进入门槛。StarExec基础设施将包括一个自定义web服务接口，连接到一个中等规模的计算集群。这个开源服务将允许多个逻辑解决社区托管基准库，运行比较不同解决方案的作业，并托管竞赛。starrexec将利用规模经济提供比大多数解决个人问题的社区可行的更复杂的服务。starrexec的一个非常重要的目标不仅仅是将不同的逻辑解决社区组合在一起，而是将它们联合起来。为此，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 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.