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

In recent years, a number of lightweight programs have been deployed incritical domains, such as in smart contracts based on blockchain technology.Therefore, the security and reliability of such programs should be guaranteedby the most credible technology. Higher-order logic theorem proving is one ofthe most reliable technologies for verifying the properties of programs.However, programs may be developed by different high-level programminglanguages, and a general, extensible, and reusable formal memory (GERM)framework that can simultaneously support different formal verificationspecifications, particularly at the code level, is presently unavailable forverifying the properties of programs. Therefore, the present work proposes aGERM framework to fill this gap. The framework simulates physical memoryhardware structure, including a low-level formal memory space, and provides aset of simple, nonintrusive application programming interfaces and assistanttools using Coq that can support different formal verification specificationssimultaneously. The proposed GERM framework is independent and customizable,and was verified entirely in Coq. We also present an extension of Curry-Howardisomorphism, denoted as execution-verification isomorphism (EVI), whichcombines symbolic execution and theorem proving for increasing the degree ofautomation in higher-order logic theorem proving assistant tools. We alsoimplement a toy functional programming language in a generalized algebraicdatatypes style and a formal interpreter in Coq based on the GERM framework.These implementations are then employed to demonstrate the application of EVIto a simple code segment.

A general formal memory framework in Coq for verifying the properties of  programs based on higher-order logic theorem proving with increased  automation, consistency, and reusability