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

Alloy is an increasingly popular lightweight specification language based onrelational logic. Alloy models can be automatically verified within a boundedscope using off-the-shelf SAT solvers. Since false assertions can usually bedisproved using small counter-examples, this approach suffices for mostapplications. Unfortunately, it can sometimes lead to a false sense ofsecurity, and in critical applications a more traditional unbounded proof maybe required. The automatic theorem prover Prover9 has been shown to beparticularly effective for proving theorems of relation algebras [7], aquantifier-free (or point-free) axiomatization of a fragment of relationallogic. In this paper we propose a translation from Alloy specifications to forkalgebras (an extension of relation algebras with the same expressive power asrelational logic) which enables their unbounded verification in Prover9. Thistranslation covers not only logic assertions, but also the structural aspects(namely type declarations), and was successfully implemented and applied toseveral examples.

Automatic Unbounded Verification of Alloy Specifications with Prover9