Our paper “Formal Specification and Model Checking of Raft Log Replication in Maude” has been accepted by DMSVIVA23. http://ksiresearchorg.ipage.com/seke/Proceedings/dms/DMSVIVA2023_Proceedings.pdf I presented at DMSVIVA23.

Our paper “Formal Specification and Model Checking of Raft Leader Election in Maude” has been accepted by ICSCA 2023. https://dl.acm.org/doi/10.1145/3587828.3587835 I presented at ICSCA 2023.

私は2020年の10月に北陸先端科学技術大学院大学 (JAIST) 先端情報科学 博士前期課程の東京社会人コースに入学しました。緒方研究室に所属しています。形式検証が主な研究テーマです。入学前から長期履修制度というものを利用することを決めていたので、2023年の9月に修了予定です。私が所属している研究室では、社会人コースのほとんどの方が長期履修制度を利用していると思います。2年でやったことを書きます。 履修した講義 JAISTでは修了するために講義で多くの単位を取得する必要があります。私は以下の講義を履修しました。 Operating Systems System Optimization Discrete Signal Processing Computer Networks Mathematical Logic Machine Learning Advanced Computer Networks

背景 機械学習を用いたシステムの信頼性・安全性を検証するためにはデータセットが必要となる。データセットの品質に偏りがあり、ノイズが入っているような低品質のデータセットに対する精度は低くなることがある。そのため、 高品質のデータセットと低品質のデータセットが混在している場合、機械学習を用いたシステムを一律に評価しても妥当性が不明瞭になるという問題がある。 …

私は2020年の10月に北陸先端科学技術大学院大学（Japan Advanced Institute of Science and Technology）先端情報科学 博士前期課程の東京社会人コースに入学しました。緒方研究室に所属しています。形式検証が主な研究テーマです。 修了するためには研究以外で20単位以上必要なので、この半年は講義の受講がメインでした。受講した講義は以下のとおりです。 システム最適化 オペレーティングシステム特論 データサイエンス論 機械学習工学 高機能コンピュータネットワーク 遠隔教育システム工学 人間力イノベーション論 創出力イノベーション論 優が7つ、良が1つでした。良があったのはとても残念でした。自習と比べると、必死に勉強しようと自然と思える点、テストやレポートを通して理解度が明確になる点、先生から興味深い話を聞ける点が良かったです。未経験のことを短期間で習得しようとすることも楽しいです。

In Maude, a module can be imported as a submodule of another in three different modes: protecting, extending, including. This is done with the syntax declarations protecting ⟨ModuleExpression⟩ . extending ⟨ModuleExpression⟩ . including ⟨ModuleExpression⟩ . which can be abbreviated, respectively, to pr ⟨ModuleExpression⟩ . ex ⟨ModuleExpression⟩ . inc ⟨ModuleExpression⟩ . The different modes of importation can be understood as promises by the user, which would need to be proved by him/herself. Before explaining each difference, I clarify no junk and no confusion. No junk is that extra values should not be added. No confusion is that different values should not be made equal.

誰? 大学では経済学を専攻していたが、大学院では情報科学の分野で研究をしたい人 社会人 プログラミング歴は約5年 受験の流れ 2020-04-19 オンラインでJapan Advanced Institute of Science and Technology(JAIST)の東京社会人コース説明会に参加した。 2020–04–22 関心のある研究室に受け入れが可能かを問うメールを送った。COVID-19のため、対面でなく、メールでやり取りすることになった。教授が発表した論文や担当している講義の資料のリンクが送られてきた。講義の単位を取得できそうとかなどについて確認するため課題を出していただくことになった。講義の資料はi217 Functional Programmingという講義のものだった。 2020–04–27 講義資料の指定された箇所を読み終わったという旨のメールを送った。1つ目の課題を出していただいた。

Let R@ be {(@1),(@2),(r1),(r2)} such that nil @ L2 = L2 (@1) (E | L1) @ L2 = E | (L1 @ L2) (@2) rev(nil) = nil (r1) rev(E | L) = rev(L) @ (E | nil) (r2) Theorem1 rev(rev(L)) = L Proof of Theorem1 by structural induction on L. Let e…

RustでBFSを練習するために、AtCoder AGC 033 A — Darker and Darker を解きました。 問題概要 「白」「黒」に塗られているH × Wのマスがあります。1 秒ごとに、各黒マスに対し、その上下左右に隣接したマスが存在するならば、そのマスを黒で塗りつぶします。全マスを黒で塗りつぶすのに何秒必要かを求めます。HとWには 1≤H,W≤1000 という制約があります。 解法 「各白マスに対して最も近い黒マスまでの距離」の中で最大の値を求めます。キューを使いたかったので、Rustでの標準ライブラリのstd::collections::VecDeque を使いました。std::collections::VecDeque にはpop_frontとpush_back があり、FIFOできます。 コードは以下のような感じで書きました。入力のマクロに関してはhttps://qiita.com/tanakh/items/0ba42c7ca36cd29d0ac8 を参照ください。