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

Heap-manipulating programs are known to be challenging to reason about. Wepresent a novel verifier for heap-manipulating programs called S2TD, whichencodes programs systematically in the form of Constrained Horn Clauses (CHC)using a novel extension of separation logic (SL) with recursive predicates anddangling predicates. S2TD actively explores cyclic proofs to address the pathexplosion problem. S2TD differentiates itself from existing CHC-based verifiersby focusing on heap-manipulating programs and employing cyclic proof toefficiently verify or falsify them with counterexamples. Compared with existingSL-based verifiers, S2TD precisely specifies the heaps of de-allocated pointersto avoid false positives in reasoning about the presence of bugs. S2TD has beenevaluated using a comprehensive set of benchmark programs from the SV-COMPrepository. The results show that S2TD is more effective than state-of-artprogram verifiers and is more efficient than most of them.

S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs