BEGIN:VCALENDAR VERSION:2.0 PRODID:-//https://techplay.jp//JP CALSCALE:GREGORIAN METHOD:PUBLISH X-WR-CALDESC:(会場と日程を変更しました) #静的コード解析 の会 第9回 X-WR-CALNAME:(会場と日程を変更しました) #静的コード解析 の会 第9回 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:710513@techplay.jp SUMMARY:(会場と日程を変更しました) #静的コード解析の会 第9回 DTSTART;TZID=Asia/Tokyo:20190302T130000 DTEND;TZID=Asia/Tokyo:20190302T180000 DTSTAMP:20260405T170757Z CREATED:20181130T211201Z DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/71051 3?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\, SyncStitch\, TLA+\, Uppaal\, VDM \, VeriFast\, Why3\, boogie\, cogent\, corral\, seL4\, vcc\, その他\n\ nしかしこれらの手法は特性が異なります。メモリの安 全性しか検査できないものや、実行バイナリを数学的 に証明できるものまで幅があるのです。実際の製品に 応用する際には「どの手法が製品のどの部分に適して いるのか」知っておく必要があります。\nまた、実際 の製品の安全性は単に設計すれば済む問題ではありま せん。お客様が製品を入手する際に、その製品はどの ような検証をなされていて、どの程度の安全性なのか 納得していただいた上で、安心して使用していただか ねばなりません。そのためにはこれらの手法をわかり やすく初学者に解説できる必要があるのです。\nこの 勉強会は上記のような静的コード解析についての意見 交換を目的としています。\n「勉強会の様子を知りた い」という場合には、発表動画から本勉強会の雰囲気 を知ることができます。\n発表スタイルと発表者の募 集\nこの勉強会では発表者を毎回募集しています。基 本的に発表者は「自分の話したい内容」を「自分の話 したい形式」で「自分の意図したレベル」にて発表で きます。無理に高度な話をする必要もありませんし、 無理に初心者にわかりやすくする必要もありません。\ nただし、初心者はわからないところを(ある程度)質問 できるものとします。おそらく初学者からは、この勉 強会で発表者が宇宙語を話しているように見えるでし ょう。ただし、主催者はあまりにも初歩的な質問内容 であった場合には任意のタイミングでその質問を打ち 切ることができることとします。\n発表者は可能であ れば当日の発表資料を後日公開してください。勉強会 に参加できなかった方々にも知見を共有したいためで す。公にしたくない内容を発表する発表者は、事前に その旨を主催者に申告してください。また、本勉強会 の発表は録画して公開する予定です。\n持ち物\n\nWindows /MacOS/LinuxいずれかのOSがインストールされ、無線LANに 接続可能なノートPC\nマウス\n少しばかりの好奇心\n\n当 日の内容\n仮ですが、以下のようなスケジュールを想 定しています。発表募集中です!\n\n13:00-14:00 「自己紹 介と今日話せるネタ出し」 by 全員\n\n\nせっかく勉強会 に集まったので、交流を深めるために自己紹介をしま しょう。持ち時間は一人3分以内です。またもし勉強会 当日に話せるネタがある場合には「XXXの発表をしたい です」と発言してください。予定を調整します。主催 者が発表ネタを作るのに苦しくなってきたので新しい ネタを供給していただけると嬉しいです!\n\n## @masterq\n\ nC言語からATS言語へのトランスレータを書きはじめま した。\n(誰が必要なんだろう？)\n\n* 「KreMLin入門 (30分) 」 by @masterq\n* 「ATS最新動向 2018年秋 (30分)」 by @masterq\n * 「VeriFastの光と闇(FreeRTOS編) (30分)」 by @masterq\n* 「C言 語からRustへの変換手法比較 (20分)」 by @masterq\n* 「TLA+ とUPPAALによって設計されたOpenComRTOS概要 (20分)」 by @mast erq\n\n## @eldesh\n\nVeriFast楽しい!\n\nネタなし\n\n## @Kuniwak\n\ nDeNAテックコンで検証の話をした。\nVDA++とSPIN。SPINい いね!\nPlusCalに興味があります。\n\nDeNAテックコンと同 じ話ならできるよ\n困ってること聞きたい! (ドメイン 固有の問題がある。。。)\n\n## @kubo39\n\nD言語いいね!\n 最近Isabelleをはじめました。\nソフトウェアの基礎をIsa belleで書きなおしている。\n\nネタなし\n\n## @ゆで卵\n\nI sabelleを最近はじたので、様子見に来たよ!\n\nネタなし\ n\n## @ntanaka-nobuakit\n\nガイオテクノロジーではたらいて ます。\nユニットテスト自動生成ツール。\nもうRustじ ゃないか？\n動的テストより、FMEAやらで人間のモデル を分析するツールが今はちょっとドメインが違うかも しれない。\n\nネタなし\n\n## @_KskSsk\n\n10年前にSPINっぽ い何かを作ってた。\nCで検証は辛い。。。\n検証は即 状態爆発になるのでは。。。\n第三の解は存在しない のか。。。\n\nネタなし\n\n## @takumi-kato\n\n量子コンピュ ータライブラリ作ってる。\n量子コンピュータもコン パイラを作る流れになるのでは。。。\n好きな言語はRu stです。\n\nネタなし\n\n## @tohdo\n\nSpark(Ada)を使ってる!\n モデル検査はまだnuSMVを使ったことがある。\n定理証明 系はLeanが好き。\nプログラムは書く毎にHaskellを勉強し なおすよ。\n\nネタなし\n\n## @ftake\n\n昔はモデル検査を 応用したツールを作ってたりした。\n最近はめっきり 。新しい情報はいつでも欲しい。\nコベリティじゃな い重くないツール欲しいですよね。\n\nネタなし\n\n## @t animocchi\n\n最近Inferを使ってる。いいね!\nCPAcheckerは関数 単位でしか使えなくてつらかった。\n\n過去に発表した 抽象解釈を使ったdeep learningの検証/学習\n\n## @tanaka_akr\n \nRubyコミッタ。Coqを使ってる。\n\nMatzの主張をCoqでデ バッグする。\nCoqのドキュメントを修正してみた。フ ォーマルじゃないドキュメントを。\n\n## @hatsugai\n\nCSP いいね! CSPのモデル検査ツールを作っている。\nIsabelle で証明を書いたりしています。\n\nネタなし\n\n## @myuon_m yon\n\n定理証明ではIsabelleを良くつかっている。昔はAgda だった。\n\nIsabelleでsortのアルゴリズムを作ったので、 その解説。\n\n## @golden_lucky\n\n鹿野と言います。ラムダ ノートで出版社。\n定理証明の本も作ってるけど、自 分で検証はしてないので、今日はROMりに来たよ。\n\nネ タなし\n\n## @khibino\n\nHaskell使ってる。Agda最近はじめま した。\n\nネタなし\n\n\n\n## 発表ネタへの投票\n\nv 10 「C 言語からRustへの変換手法比較 (20分)」 by @masterq\nv 10 Mat zの主張をCoqでデバッグする。\nv 10 Isabelleでsortのアル ゴリズムを作ったので、その解説。\nv 9 「TLA+とUPPAALに よって設計されたOpenComRTOS概要 (20分)」 by @masterq\nv 7 過 去に発表した抽象解釈を使ったdeep learningの検証/学習\n v 6 DeNAテックコンと同じ話ならできるよ\nv 6 「ATS最新 動向 2018年秋 (30分)」 by @masterq\nv 4 Coqのドキュメントを 修正してみた。フォーマルじゃないドキュメントを。\ nv 5 「VeriFastの光と闇(FreeRTOS編) (30分)」 by @masterq\n4 「Kr eMLin入門 (30分)」 by @masterq\n\n\n\n\n\n「懇親会の調整 (お 店を選んで参加人数で予約します) (15分) 」by 全員\n\n\n 「KreMLin入門 (30分)」 by @masterq\n\n\n\nF*のサブセットで、 C言語にコンパイルできるLow*のコンパイラを、KreMLinユ ーザマニュアル http://fstar-ja.metasepi.org/doc/kremlin-book/ を 読みながら入門します。\n\n\n「ATS最新動向 2018年秋 (30 分)」 by @masterq\n\n\n一時期話題になったATS言語。2018年 に入って「ATS3の設計開始宣言」と「Vanessa‍ McHaleがATS 使いになった」ことでATS言語界隈は大きく変わる兆し がありました。ATS3の最新動向とVanessa‍が設計したツ ール群について簡単に紹介します。当日の資料はこち らです。\n\n\n「VeriFastの光と闇(FreeRTOS編) (30分)」 by @mas terq\n\n\n@masterqがFreeRTOSのタスクを少しだけVeriFastで検証 してみました。その結果実感したVeriFastの良い面と悪 い面について共有します。当日の資料はこちらです。\ n\n\n「C言語からRustへの変換手法比較 (20分)」 by @masterq\ n\n\nC言語からRustへの変換手法としてcorrodeとc2rustが広 く知られています。前者は純粋なHaskell実装で、後者は Rust+Clang+Emscriptenで実現されています。両者の比較のた めにBSD catコマンドを両ツールでRustに変換してみまし た。変換してcorrodeの結果とc2rustの結果が得られました 。変換結果を眺めながらCFGの特性などを比較します。 また発表者は変換結果をrustcでコンパイルできなかっ たので助言がいただけると助かります。\n\n\n「TLA+とUPP AALによって設計されたOpenComRTOS概要 (20分)」 by @masterq\n\ n\nOpenComRTOSというRTOSはTLA+とUPPAALという2つのツールに よって設計されています。TLA+はモデル検査に、UPPAALは 性能モデル検証に用いられています。Formal Development of a Network-Centric RTOSというレポートを読みながらモデル検 査のRTOSへの適用事例と発表者の感想を共有します。\n\ n\n17:45-18:00 「次回の計画 (15分)」 by 全員\n\n会場につい て\nサイボウズ様に会議室を提供していただきました 。ありがとうございます!\n\n場所: 東京都中央区日本橋 2-7-1 東京日本橋タワー\n別途メールにて連絡する手順 で入館してください\n電源、Wi-Fi は自由に使えます。\n 飲食は自由です。\nその他この勉強会において困った ことがありましたら 090-3524-7064 まで電話をください。 主催者 が対応いたします。\n\n懇親会\n18:30から懇親会 を開催します。\n建設的な議論のために\n主催者自身が 建設的な議論を阻害しがちなので、議論のやり方につ いてルールを導入しようとしています。\n今回の勉強 会では具体的なルールを制定しませんが、参加者一人 一人が以下の文書を読むことを推奨します。\nまた本 勉強会で困ったことなどご意見がありましたらMetasepi メーリングリストまでご連絡ください。対応いたしま す。\nRust行動規範\nコミュニティに参加する全員が尊 守すべきルールです。\nこの文書はRustコミュニティに 向けたものですが、本勉強会が大規模化するにあたり 、参考にして独自の行動規範を導入する予定です。\n はじめてのBillGレビューのこと\nビル・ゲイツは仕様書 のレビューの際に以下のように語ったそうです。\n\n「 これをどうやって実現するのか本当に詳細に調べた者 が誰かいるのか? たとえば、日付と時刻に関するあの たくさんの関数だ。Excelには日付と時刻の関数がすご くたくさんある。Basicが同じ関数を持つようになるの か? それが全部同じように動くようになるのか?」 \n\n 私達は研究者ではありません。製品を設計する技術者 です。理学ではなく工学に属するのです。\nまた論文 に書いてあることや有識者の見解を鵜呑みにすること は実際の製品を作る上で危険です。「この技術は本当 に動くのか？」という疑念を常に持ちましょう。\n実 際に技術に触れ、使ってみて、実装を読まなけれ真実 は見えません。\nファスト＆スロー\n人間の脳は素早い 判断を行なうシステム1と熟慮して論理的に考えるシス テム2があるそうです。\nシステム1ではなくシステム2 で考えてから発言することを心掛けましょう。\n(もっ とも主催者自身がシステム1ばかり使ってしまう傾向が あるのですが。。。)\n協賛\n\nサイボウズ株式会社様: 会場の提供\n LOCATION:サイボウズ株式会社 東京都中央区日本橋2-7-1 (東 京日本橋タワー) URL:https://techplay.jp/event/710513?utm_medium=referral&utm_source=ics&utm _campaign=ics END:VEVENT END:VCALENDAR