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

We introduce a new dynamic analysis technique to discover invariants inseparation logic for heap-manipulating programs. First, we use a debugger toobtain rich program execution traces at locations of interest on sample inputs.These traces consist of heap and stack information of variables that point todynamically allocated data structures. Next, we iteratively analyze separatememory regions related to each pointer variable and search for a formula overpredefined heap predicates in separation logic to model these regions. Finally,we combine the computed formulae into an invariant that describes the shape ofexplored memory regions.  We present SLING, a tool that implements these ideas to automaticallygenerate invariants in separation logic at arbitrary locations in C programs,e.g., program pre and postconditions and loop invariants. Preliminary resultson existing benchmarks show that SLING can efficiently generate correct anduseful invariants for programs that manipulate a wide variety of complex datastructures.

SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic