Certora、木曜午前11時(米東部時間)にAutoProverをライブ解説

このセッションにはCEOのSagiv Mooly氏が登壇し、コードを読み取り、仕様を生成して検証するよう設計された形式検証システム「AutoProver」に焦点を当てる。

要約

Certoraは、木曜午前11時(米東部時間)にCEOのSagiv Mooly氏を迎えたライブ討論を開催すると発表した。セッションでは、同社の最新リリースであるAutoProverを取り上げる予定で、同社はこれをコードを読み取り、仕様を生成して検証するエージェント型の形式検証システムと説明している。形式検証(数学的なコード検証)は、特にセキュリティ上の重要性が高い仮想通貨アプリケーションにおいて、ソフトウェアが意図通りに動作するかを検証するために一般的に用いられている。

用語解説
  • AutoProver: Certoraのコード検証向け形式検証システム。
  • formal verification: ソフトウェアが意図した挙動と一致するかを数学的に検証すること。