C言語検証器 #VeriFast 入門 第1回
2016/07/22(金)18:30
〜
21:30
開催
ブックマーク
イベント内容
概要
VeriFast はシングルスレッドやマルチスレッドのC言語プログラムの性質が正しいことを検証するプログラム検証ツールです。 このツールはC言語プログラムを読み、「エラーが見つからなかった」とレポートするかエラーの可能性がある位置を示します。もしこのツールが「エラーが見つからなかった」とレポートしたなら、そのプログラムは次のようであることを意味しています:
- 構造体インスタンスが解放された後にその構造体のフィールドを読み書きすることや、もしくは配列の終端を超えた読み書きのような、不正なメモリアクセスを行ないません
- データレース、すなわちマルチスレッドによる同じフィールドへの非同期な競合アクセス、として知られたある種の並行性のエラーを含みません
- 関数は、そのソースコード中の特殊なコメントでプログラマによって指示された、事前条件と事後条件に従っています
本勉強会は、VeriFastに入門することを目的とした VeriFastチュートリアル(翻訳) の読書会です。勉強会ではこの文書を頭から読み進めます。
事前準備
https://people.cs.kuleuven.be/~bart.jacobs/verifast/ からお使いのOSに対応したVeriFastをダウンロードし、インストールしておいてください。また vfide
コマンドを使ってVeriFast IDEが起動することを確認してください。
もしどうしてもVeriFastのインストールができなかった方は、そのまま勉強会に参加してください。会場で簡単にインストール方法を説明します。
今回の内容
今回は、勉強会の発起人である 岡部 がVeriFastチュートリアルの日本語訳を、前回の続きである 6章 から朗読します。以下のようなスケジュールを予定しています。
- 18:30-18:45: 本勉強会の趣旨、主にVeriFastを学ぶ動機についてを簡単に説明します。
- 18:45-20:00: VeriFastチュートリアルを読みます。必要ならVeriFastのインストール方法を解説します。
- 20:15-21:15: 休憩をはさんで、VeriFastチュートリアル読みを再開します。
- 21:15-21:30: 次回勉強会の予定を立てます。
- 22:00-23:00: 有志で懇親会を行ないます。
会場について
- 会場: ライフロボティクス株式会社
- 住所: 東京都江東区富岡二丁目9番11号 京福ビル5階
会場では無線LANを利用できる予定です。
注意事項
※ こちらのイベント情報は、外部サイトから取得した情報を掲載しています。
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。