【OSS】Microsoft、スマートコントラクト検証ツール「VeriSol」をオープンソース公開---高カバレッジの記号テストをサポート

【OSS】Microsoft、スマートコントラクト検証ツール「VeriSol」をオープンソース公開---高カバレッジの記号テストをサポート

OSS×クラウド最新TOPICS 2019年6月6日 13:11

【OSS】Microsoft、スマートコントラクト検証ツール「VeriSol」をオープンソース公開---高カバレッジの記号テストをサポート

Microsoftは、スマートコントラクト検証ツール「VeriSol」をオープンソース公開した。

「VeriSol」とは

「VeriSol(Verifier for Solidity)」はスマートコントラクト用の正式な検証および分析システムのプロトタイプを作成するためのMicrosoft Researchプロジェクト。

→GitHub →microsoft/verisol

プログラミング言語「Solidity」を利用

「Solidity」は、Ethereumプラットフォームでスマートコントラクトを実装するための高級言語で、「静的型付け」「コントラクト指向」などの特徴を持つ。

→GitHub →ethereum/solidity

「VeriSol」は、Solidityプログラムのセマンティクスを正式な中間検証言語「Boogie」にエンコードし、Boogie検証ツールチェーンを活用し拡張することによって動作する。

高カバレッジの記号テストをサポート

「VeriSol」は、反例の痕跡を自動的に見つけるための高カバレッジの記号テストをサポートしている。

また、自動的に正確さの証明を実行できる。

以上、下記URLからの要約
https://www.microsoft.com/en-us/research/blog/researchers-work-to-secure-azure-blockchain-smart-contracts-with-formal-verification/?ocid=msr_blog_verisol_tw

OSSNEWSに広告を掲載しませんか?

関連オープンソース

Catalyst(カタリスト)

  • FinTech系ツール

Catalyst(カタリスト)とは、暗号通貨トレーディングアルゴリズムライブラリです。

Hyperledger(ハイパーレッジャー)

  • FinTech系ツール

Hyperledger(ハイパーレッジャー)とは、オープンソース「ブロックチェーン技術推進コミュニティー」です。「Linux Foundation」が中心となり、世界30以上の先進的IT企業が協力して、ブロックチェーン技術/P2P分散レッジャー技術の確立を目指しています。

  • オープソース書籍(サイド)
  • OSSNEWSに広告を掲載しませんか?

facebook

twitter

facebook

twitter