BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//https://techplay.jp//JP
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALDESC:#静的コード解析の会 第5回@北海道
X-WR-CALNAME:#静的コード解析の会 第5回@北海道
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:620497@techplay.jp
SUMMARY:#静的コード解析の会 第5回@北海道
DTSTART;TZID=Asia/Tokyo:20170716T123000
DTEND;TZID=Asia/Tokyo:20170716T180000
DTSTAMP:20260517T220310Z
CREATED:20170430T161516Z
DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/62049
 7?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\n静的コード
 解析とこの勉強会について\n静的コード解析をご存知
 でしょうか。静的コード解析とは、コンピュータのソ
 フトウェアの解析手法の一種で、ソフトウェアを実行
 することなく解析を行うことです。このような手法に
 は以下のように様々な実装があります:\n\nATS\, CBMC\, Coq\
 , Coverity Scan\, CSP\, Dafny\, F*\, Frama-C\, FreeSafeTy\, Infer\, Isabe
 lle\, SATABS\, Spin\, Uppaal\, 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:30-13:00 開場\n13:00-14:00 「ChibiOS/RT開発環
 境の構築」 by @masterq\n\n\nメジャーなRTOSの1つであるChibi
 OS/RTを紹介し、参加者のPCにそのビルド環境を構築しま
 す。ビルド構築について詳しくはchibios-verifastリポジト
 リを参照してください。\n\n\n14:00-14:10 休憩\n14:10-15:10 
 「STマイクロ製マイコンボード上におけるChibiOS/RTアプ
 リケーションの実行」 by @masterq\n\n\nメジャーなマイコ
 ンメーカの1つであるSTマイクロ製のボードを使って、
 前タームで構築したChibiOS/RTのアプリケーションを動作
 させます。\n\n\n15:10-15:20 休憩\n15:20-15:35 懇親会の調整 (
 お店を選んで参加人数で予約します)\n15:35-16:35 「VeriFas
 tによるChibiOS/RTアプリケーションの検証」 by @masterq\n\n\
 n前タームで使用したChibiOS/RTアプリケーションのコー
 ドに対してVeriFastを使って簡単な検証を行ないます。\n
 \n\n16:35-16:45 休憩\n16:45-17:40 「未定」\n\n\n当日までに予
 定が決まらなければ、各自もくもく会になります。参
 加者が「こんな検証をしてみたい」と提案して、それ
 に対して検証可能かどうか皆で調べるのも面白いかも
 しれません。\n\n\n17:40-18:00 次回の計画\n\nしかし会場か
 らの活発な議論があった場合などは柔軟に対応しよう
 と考えています。\n会場について\n未定\n懇親会\n18:30か
 ら懇親会を開催します。\n協賛\n\nSTマイクロエレクト
 ロニクス様: マイコンボードの提供\n
LOCATION:オンライン
URL:https://techplay.jp/event/620497?utm_medium=referral&utm_source=ics&utm
 _campaign=ics
END:VEVENT
END:VCALENDAR
