论文标题
公式：用于基于SMT的静态分析的数据元（扩展版）
Formulog: Datalog for SMT-Based Static Analysis (Extended Version)
论文作者
论文摘要
令人满意的模型理论（SMT）解决已成为许多静态分析的关键部分，包括符号执行，改进类型检查和模型检查。我们提出了一种特定于领域的语言的公式，它使得可以以接近其正式规范的方式编写一系列基于SMT的静态分析，并且可以适应高级优化和有效的评估。 公式使用一阶功能语言和用于表示SMT公式的一阶功能语言和机制扩展了逻辑编程语言数据。一种新型类型的系统支持表达公式的构建，同时确保既没有正常的评估和解决SMT解决问题。我们的案例研究表明，一系列基于SMT的分析可以自然而简洁地编码在Formulog中，并且 - 借助此编码 - 高级数据型式优化可以自动且有利地应用于这些分析。
Satisfiability modulo theories (SMT) solving has become a critical part of many static analyses, including symbolic execution, refinement type checking, and model checking. We propose Formulog, a domain-specific language that makes it possible to write a range of SMT-based static analyses in a way that is both close to their formal specifications and amenable to high-level optimizations and efficient evaluation. Formulog extends the logic programming language Datalog with a first-order functional language and mechanisms for representing and reasoning about SMT formulas; a novel type system supports the construction of expressive formulas, while ensuring that neither normal evaluation nor SMT solving goes wrong. Our case studies demonstrate that a range of SMT-based analyses can naturally and concisely be encoded in Formulog, and that -- thanks to this encoding -- high-level Datalog-style optimizations can be automatically and advantageously applied to these analyses.
