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 Plus annual

Presents the access of premium content as premium feature

Premium Content

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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Expressive state-of-the-art separation logics rely on step-indexing to modelsemantically complex features and to support modular reasoning about imperativehigher-order concurrent and distributed programs. Step-indexing comes, however,with an inherent cost: it restricts the adequacy theorem of program logics to afairly simple class of safety properties. In this paper, we explore if and howintensional refinement is a viable methodology for strengthening higher-orderconcurrent (and distributed) separation logic to prove non-trivial safety andliveness properties. Specifically, we introduce Trillium, a language-agnosticseparation logic framework for showing intensional refinement relations betweentraces of a program and a model. We instantiate Trillium with a concurrentlanguage and develop Fairis, a concurrent separation logic, that we use to showliveness properties of concurrent programs under fair scheduling assumptionsthrough a fair liveness-preserving refinement of a model. We also instantiateTrillium with a distributed language and obtain an extension of Aneris, adistributed separation logic, which we use to show refinement relations betweendistributed systems and TLA+ models.

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement