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

This paper presents a theory of skiplists of arbitrary height, and showsdecidability of the satisfiability problem for quantifier-free formulas.  A skiplist is an imperative software data structure that implements sets bymaintaining several levels of ordered singly-linked lists in memory, where eachlevel is a sublist of its lower levels. Skiplists are widely used in practicebecause they offer a performance comparable to balanced binary trees, and canbe implemented more efficiently. To achieve this performance, mostimplementations dynamically increment the height (the number of levels).Skiplists are difficult to reason about because of the dynamic size (number ofnodes) and the sharing between the different layers. Furthermore, reasoningabout dynamic height adds the challenge of dealing with arbitrary many levels.  The first contribution of this paper is the theory TSL that allows to expressthe heap memory layout of a skiplist of arbitrary height. The secondcontribution is a decision procedure for the satisfiability prob- lem ofquantifier-free TSL formulas. The last contribution is to illustrate the formalverification of a practical skiplist implementation using this decisionprocedure.

A Decidable Theory of Skiplists of Unbounded Size and Arbitrary Height