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

Relational properties describe multiple runs of one or more programs. Theycharacterize many useful notions of security, program refinement, andequivalence for programs with diverse computational effects, and they havereceived much attention in the recent literature. Rather than developingseparate tools for special classes of effects and relational properties, weadvocate using a general purpose proof assistant as a unifying framework forthe relational verification of effectful programs. The essence of our approachis to model effectful computations using monads and to prove relationalproperties on their monadic representations, making the most of existingsupport for reasoning about pure programs.  We apply this method in F* and evaluate it by encoding a variety ofrelational program analyses, including information flow control, programequivalence and refinement at higher order, correctness of programoptimizations and game-based cryptographic security. By relying on SMT-basedautomation, unary weakest preconditions, user-defined effects, and monadicreification, we show that, compared to unary properties, verifying relationalproperties requires little additional effort from the F* programmer.

A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations