TOP

C言語検証器 #VeriFast 入門 第0回

イベント内容

概要

VeriFast はシングルスレッドやマルチスレッドのC言語プログラムの性質が正しいことを検証するプログラム検証ツールです。 このツールはC言語プログラムを読み、「エラーが見つからなかった」とレポートするかエラーの可能性がある位置を示します。もしこのツールが「エラーが見つからなかった」とレポートしたなら、そのプログラムは次のようであることを意味しています:

  • 構造体インスタンスが解放された後にその構造体のフィールドを読み書きすることや、もしくは配列の終端を超えた読み書きのような、不正なメモリアクセスを行ないません
  • データレース、すなわちマルチスレッドによる同じフィールドへの非同期な競合アクセス、として知られたある種の並行性のエラーを含みません
  • 関数は、そのソースコード中の特殊なコメントでプログラマによって指示された、事前条件と事後条件に従っています

本勉強会は、VeriFastに入門することを目的とした VeriFastチュートリアル(翻訳) の読書会です。勉強会ではこの文書を頭から読み進めます。

事前準備

https://people.cs.kuleuven.be/~bart.jacobs/verifast/ からお使いのOSに対応したVeriFastをダウンロードし、インストールしておいてください。また vfide コマンドを使ってVeriFast IDEが起動することを確認してください。

もしどうしてもVeriFastのインストールができなかった方は、そのまま勉強会に参加してください。会場で簡単にインストール方法を説明します。

今回の内容

初回である今回は、勉強会の発起人である 岡部 がこの勉強会の趣旨説明と、VeriFastチュートリアルの日本語訳を1章から朗読します。以下のようなスケジュールを予定しています。

  • 18:30-19:00: 本勉強会の趣旨、主にVeriFastを学ぶ動機についてを簡単に説明します。
  • 19:00-20:00: VeriFastチュートリアルを読みます。必要ならVeriFastのインストール方法を解説します。
  • 20:15-21:15: 休憩をはさんで、VeriFastチュートリアル読みを再開します。
  • 21:15-21:30: 次回勉強会の予定を立てます。
  • 22:00-23:00: 有志で懇親会を行ないます。

会場について

  • 会場: ライフロボティクス株式会社
  • 住所: 東京都江東区富岡二丁目9番11号 京福ビル5階

会場では無線LANを利用できる予定です。

参加者
5人 /定員6人
申込先
会場
ライフロボティクス株式会社
東京都江東区富岡二丁目9番11号 京福ビル5階

注目のイベント

タグに関連するイベント

コラム

イベント New

インメモリデータベースの今後。新領域への適用可能性 - デジタルトランスフォーメーション時代の最新データベース技術勉強会 -

2018年3月6日(火)19時10分より、「【エンジニア向け勉強会】デジタルトランスフォーメーション時代の最新...
162 views
インタビュー

【eiicon×サムライインキュベート】事業創出支援「Open Innovation BootCamp Program」スタート!

ここ数年で、オープンイノベーションに対する企業の関心は急速に高まっている。しかしながら、「どうしたら...
110 views
イベント

4月(後半)に開催する注目のITイベント・勉強会まとめ 28選

4月後半に開催される注目のITイベント・勉強会をまとめました! 気になるイベントがあれば是非ご参加くだ...
1,624 views