BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//https://techplay.jp//JP
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALDESC:#静的コード解析の会 第7回
X-WR-CALNAME:#静的コード解析の会 第7回
X-WR-TIMEZONE:Asia/Tokyo
BEGIN:VTIMEZONE
TZID:Asia/Tokyo
BEGIN:STANDARD
DTSTART:19700101T000000
TZOFFSETFROM:+0900
TZOFFSETTO:+0900
TZNAME:JST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:661716@techplay.jp
SUMMARY:#静的コード解析の会 第7回
DTSTART;TZID=Asia/Tokyo:20180512T124500
DTEND;TZID=Asia/Tokyo:20180512T180000
DTSTAMP:20260507T052257Z
CREATED:20180228T211137Z
DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/66171
 6?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\n静的コード
 解析とこの勉強会について\n静的コード解析をご存知
 でしょうか。静的コード解析とは、コンピュータのソ
 フトウェアの解析手法の一種で、ソフトウェアを実行
 することなく解析を行うことです。このような手法に
 は以下のように様々な実装があります:\n\nATS\, B-Method\, 
 CBMC\, Coq\, Coverity Scan\, CSP\, Dafny\, F*\, Frama-C\, FreeSafeTy\, In
 fer\, Isabelle\, SATABS\, SPARK\, Spin\, Uppaal\, VDM\, VeriFast\, Why3\,
  boogie\, cogent\, corral\, seL4\, vcc\, その他\n\nしかしこれら
 の手法は特性が異なります。メモリの安全性しか検査
 できないものや、実行バイナリを数学的に証明できる
 ものまで幅があるのです。実際の製品に応用する際に
 は「どの手法が製品のどの部分に適しているのか」知
 っておく必要があります。\nまた、実際の製品の安全
 性は単に設計すれば済む問題ではありません。お客様
 が製品を入手する際に、その製品はどのような検証を
 なされていて、どの程度の安全性なのか納得していた
 だいた上で、安心して使用していただかねばなりませ
 ん。そのためにはこれらの手法をわかりやすく初学者
 に解説できる必要があるのです。\nこの勉強会は上記
 のような静的コード解析についての意見交換を目的と
 しています。\n発表スタイルと発表者の募集\nこの勉強
 会では発表者を毎回募集しています。基本的に発表者
 は「自分の話したい内容」を「自分の話したい形式」
 で「自分の意図したレベル」にて発表できます。無理
 に高度な話をする必要もありませんし、無理に初心者
 にわかりやすくする必要もありません。\nただし、初
 心者はわからないところを(ある程度)質問できるもの
 とします。おそらく初学者からは、この勉強会で発表
 者が宇宙語を話しているように見えるでしょう。ただ
 し、主催者はあまりにも初歩的な質問内容であった場
 合には任意のタイミングでその質問を打ち切ることが
 できることとします。\n発表者は可能であれば当日の
 発表資料を後日公開してください。勉強会に参加でき
 なかった方々にも知見を共有したいためです。公にし
 たくない内容を発表する発表者は、事前にその旨を主
 催者に申告してください。\n持ち物\n\nWindows/MacOS/Linuxい
 ずれかのOSがインストールされ、無線LANに接続可能な
 ノートPC\n\n当日の内容\n仮ですが、以下のようなスケ
 ジュールを想定しています。\n\n12:45 ビル1階のファミ
 リーマート飲食スペースに集合してください\n13:00-14:00
  「自己紹介と今日話せるネタ出し」 by 全員\n\n\nせっ
 かく勉強会に集まったので、交流を深めるために自己
 紹介をしましょう。持ち時間は一人5分以内です。また
 もし勉強会当日に話せるネタがある場合には「XXXの発
 表をしたいです」と発言してください。予定を調整し
 ます。主催者が発表ネタを作るのに苦しくなってきた
 ので新しいネタを供給していただけると嬉しいです!\n\
 n## 自己紹介\n\n### masterq\n\nFPGA屋さんになっている。Viva
 doなれない。。。\n\n今日のネタ:\n\n* さわって学ぶVCC(VC
 Cチュートリアルの翻訳) 60分\n\n### hatsugai\n\n仕事ないぞ
 。ひからびる。\n趣味のプログラミングに忙しい。\nネ
 タないよ!\n\n### tos\n\n最近仕事に復帰。一週間目!\n4月
 頭からトップエスイーに通いはじめたよ。\n\nhttps://www.
 topse.jp/ja/\n\n命題論理/述語論理/ホーア論理など基礎を
 やってから、静的解析の紹介などがあったよ。\n(岡部
 はちゃんと基礎がないまま勉強会運営しているよ)\n\n##
 # khibino\n\nHaskellで仕事しているよ。\nflopsに行ってきた
 よ。\n\n今日のネタ:\n\n* flopsでわかったことをざっくり
 でなら話せるよ 30分\n\n### tanimocchi\n\nセキュリティ屋さ
 んだよ。暗号とか。分散やら。\n\n今日のネタ:\n\n* flops
 のネタのサポートなら\n\n### ftake\n\n普段はansible屋さん
 に今なってるよ。\n今日のネタ、、、つらみ。。。\n\n
 今日のネタ:\n\n* 皆で https://sv-comp.sosy-lab.org/2018/ を眺め
 る 20分\n\n### 久保秋 真\n\nUMLのツール作ってるよ。\n最
 近別の仕事で動的解析のツールを試してたよ。\n組み
 込みだと動的解析がつらい。。。\nETロボコンの仕事を
 しなければ。。。\nCygwinのインストールやらITリテラシ
 ー教育の重みもデカい。\nトップエスイーでモデル駆
 動開発をやってて、その記事を昔書いたよ。\n2018-05-18
 にC言語の入門本を出版するよ:\n\nhttps://www.amazon.co.jp/dp/
 4802611587\n\n### eldesh\n\nネタないよ。\nflopsに行ってきた
 よ。\n機械学習の会社でWebサービスを作っているよ。Ru
 stで。\nVeriFastがまだマイブームでキテるよ。\nもっと
 基礎的な教科書を読もうとしていて、ホーア論理を学
 習中。\n\n\n\n14:00以降は各自の持ちネタを発表します。
 途中休憩を10分x2確保しようと思います。現時点で上が
 っている発表ネタとその発表に必要な時間は以下です:
 \n\n「皆で https://sv-comp.sosy-lab.org/2018/ を眺める (20分)」\
 n「 http://www.sqlab.jp/FLOPS2018/ でわかったことをざっくり
 でなら話せるよ (30分)」\n「さわって学ぶVCC (60分以上)
 」 by @masterq\n\n\nVCCはMicrosoft Research製のC言語静的解析ツ
 ールです。C言語に_(foo)という特殊な注釈を挿入して、
 コードの正しさを検証します。本発表ではVCCのチュー
 トリアルである"Verifying C Programs: A VCC Tutorial"で紹介さ
 れたコードをオンラインで実行させながらVCCの使い方
 を学びます。左記チュートリアルのざっくりとした翻
 訳もあります。\n"5 Object invariants"の後半まで読みまし
 た。\n\n\n「懇親会の調整 (お店を選んで参加人数で予
 約します) (15分) 」by 全員\n17:45-18:00 「次回の計画 (15分
 )」 by 全員\n\n会場について\n永和システムマネジメン
 ト様に会議室を提供していただきました。ありがとう
 ございます!\n\n場所 : 〒101‐0041 東京都千代田区神田須
 田町2-3-1 NBF神田須田町ビル7F map（1階がファミリーマー
 トのビルです。）\n\n開催日は休日のため、ビル自体が
 入館制限されており、関係者でないと入れません ので
 注意ください。\n参加者のみなさんは次の段取りに従
 って入館してください。\n\n12:45 に同ビル1階のファミ
 リーマートの飲食スペースあたりに集合してください
 。\n入館できる人が引率して、まとまって入館します
 。\n遅参した場合は、ファミリーマートに到着したら 0
 90-3524-7064 まで電話してください。別途入館を支援しま
 す。\n主催・発表予定者で、早めに来たい方には、別
 途調整しますのでご連絡ください(会場は 12:30 から使
 えるようにしてあります)。\n電源、Wi-Fi は自由に使え
 ます。\n飲食は自由です。自動販売機があります。（
 ゴミの後始末は各自でお願いします。）\nその他この
 勉強会において困ったことがありましたら 090-3524-7064 
 まで電話をください。主催者 が対応いたします。\n\n
 懇親会\n18:30から以下で懇親会を開催します。\n\n春天
 酒坊 03-6206-9200 東京都千代田区神田須田町2-6-2-101\n\n協
 賛\n\n永和システムマネジメント様: 会場の提供\n
LOCATION:永和システムマネジメント コワーキングスペー
 ス 東京都千代田区神田須田町2-3-1 NBF神田須田町ビル7F
URL:https://techplay.jp/event/661716?utm_medium=referral&utm_source=ics&utm
 _campaign=ics
END:VEVENT
END:VCALENDAR