论文标题
基础进行定量分离逻辑（扩展版本）的基础
Foundations for Entailment Checking in Quantitative Separation Logic (extended version)
论文作者
论文摘要
定量分离逻辑（QSL）是用于验证概率指针程序的分离逻辑（SL）的扩展。在QSL中，公式对实数，而不是真实价值，例如，在给定的符号堆中内存安全终止的可能性。与\ sl一样，当用QSL推理为\ emph {intailment}时，关键问题之一：公式f是否需要另一个公式g？ 我们从QSL中进行综合减少，再到SL中的需要检查。这允许大量SL研究来自动验证概率指针程序。我们分析方法的复杂性并证明其适用性。特别是，我们通过将我们的还原应用于分离逻辑的众所周知的符号 - 高位片段的定量扩展，从而获得了对此类程序进行验证的第一个可决定性结果。
Quantitative separation logic (QSL) is an extension of separation logic (SL) for the verification of probabilistic pointer programs. In QSL, formulae evaluate to real numbers instead of truth values, e.g., the probability of memory-safe termination in a given symbolic heap. As with \SL, one of the key problems when reasoning with QSL is \emph{entailment}: does a formula f entail another formula g? We give a generic reduction from entailment checking in QSL to entailment checking in SL. This allows to leverage the large body of SL research for the automated verification of probabilistic pointer programs. We analyze the complexity of our approach and demonstrate its applicability. In particular, we obtain the first decidability results for the verification of such programs by applying our reduction to a quantitative extension of the well-known symbolic-heap fragment of separation logic.
