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 present a tool for verification of deterministic programs with sharedmutable references against specifications such as assertions, preconditions,postconditions, and read/write effects. We implement our tool by encodingprograms with mutable references into annotated purely functional recursiveprograms. We then rely on function unfolding and the SMT solver Z3 to prove ordisprove safety and to establish program termination. Our tool uses a newtranslation of programs where frame conditions are encoded usingquantifier-free formulas in first-order logic (instead of relying onquantifiers or separation logic). This quantifier-free encoding enables SMTsolvers to prove safety or report counterexamples relative to the semantics ofprocedure specifications. Our encoding is possible thanks to the expressivepower of the extended array theory of the Z3 SMT solver. In addition to theability to report counterexamples, our tool retains efficiency of reasoningabout purely functional layers of data structures, providing expressiveness formutable data but also a significant level of automation for purely functionalaspects of software. We illustrate our tool through examples manipulatingmutable linked structures and arrays.

Proving and Disproving Programs with Shared Mutable Data