English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Quantitative separation logic (QSL) is an extension of separation logic (SL)for the verification of probabilistic pointer programs. In QSL, formulaeevaluate to real numbers instead of truth values, e.g., the probability ofmemory-safe termination in a given symbolic heap. As with \SL, one of the keyproblems when reasoning with QSL is \emph{entailment}: does a formula f entailanother formula g?  We give a generic reduction from entailment checking in QSL to entailmentchecking in SL. This allows to leverage the large body of SL research for theautomated verification of probabilistic pointer programs. We analyze thecomplexity of our approach and demonstrate its applicability. In particular, weobtain the first decidability results for the verification of such programs byapplying our reduction to a quantitative extension of the well-knownsymbolic-heap fragment of separation logic.

Foundations for Entailment Checking in Quantitative Separation Logic (extended version)