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/

Zendy Plus

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

Zendy Tools

Zendy Open

The growing adoption of smart contracts on blockchains poses new securityrisks that can lead to significant monetary loss, while existing approacheseither provide no (or partial) security guarantees for smart contracts orrequire huge proof effort. To address this challenge, we present SciviK, aversatile framework for specifying and verifying industrial-grade smartcontracts. SciviK's versatile approach extends previous efforts with three keycontributions: (i) an expressive annotation system enabling built-in directivesfor vulnerability pattern checking, neural-based loop invariant inference, andthe verification of rich properties of real-world smart contracts (ii) afine-grained model for the Ethereum Virtual Machine (EVM) that provideslow-level execution semantics, (iii) an IR-level verification frameworkintegrating both SMT solvers and the Coq proof assistant.  We use SciviK to specify and verify security properties for 12 benchmarkcontracts and a real-world Decentralized Finance (DeFi) smart contract. Amongall 158 specified security properties (in six types), 151 properties can beautomatically verified within 2 seconds, five properties can be automaticallyverified after moderate modifications, and two properties are manually provedwith around 200 lines of Coq code.

SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts