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

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

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

The verification systems Boogie and Why3 use their respective intermediatelanguages to generate verification conditions from high-level programs. Sincethe two systems support different back-end provers (such as Z3 and Alt-Ergo)and are used to encode different high-level languages (such as C# and Java),being able to translate between their intermediate languages would provide away to reuse one system's features to verify programs meant for the other. Thispaper describes a translation of Boogie into WhyML (Why3's intermediatelanguage) that preserves semantics, verifiability, and program structure to alarge degree. We implemented the translation as a tool and applied it to 194Boogie-verified programs of various sources and sizes; Why3 verified 83% of thetranslated programs with the same outcome as Boogie. These results indicatethat the translation is often effective and practically applicable.

Why Just Boogie? Translating Between Intermediate Verification Languages