Open in app

Sign In

Write

Sign In

Takanori Ishibashi
Takanori Ishibashi

52 Followers

Home

About

Sep 19

JAISTの博士前期課程修了 & 博士後期課程進学

2023年の9月にJAISTの博士前期課程東京社会人コースを修了しました。分散合意プロトコルRaftの形式仕様とモデル検査というテーマで学位論文を書きました。博士前期課程は入学試験で話した研究テーマに沿って研究を進めましたが、ある課題に直面したため、目標としていたことの一部を達成できませんでした。 研究を進めていく中で国際学会論文を2本が採択されました。https://scholar.google.co.jp/citations?user=Tt04xmgAAAAJ&hl=ja 2023年の10月からJAISTの博士後期課程に進学します。博士前期課程の研究で直面した課題を解決できるような手法を提案しようとしてます。

1 min read

1 min read


Jun 29

Formal Specification and Model Checking of Raft Log Replication in Maude

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.

Computer Science

1 min read

Computer Science

1 min read


Jun 20

Formal Specification and Model Checking of Raft Leader Election in Maude

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.

1 min read

Formal Specification and Model Checking of Raft Leader Election in Maude
Formal Specification and Model Checking of Raft Leader Election in Maude

1 min read


Oct 4, 2022

社会人大学院生になって2年経過した

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

6 min read

6 min read


Dec 4, 2021

機械学習を用いたシステムの分析・統計的な評価

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

Machine Learning

10 min read

機械学習を用いたシステムの分析・統計的な評価
機械学習を用いたシステムの分析・統計的な評価
Machine Learning

10 min read


Apr 12, 2021

社会人大学院生になって半年経過した

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

2 min read

2 min read


Sep 8, 2020

Module importations in Maude

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.

Maude

1 min read

Maude

1 min read


Aug 29, 2020

JAIST社会人コース受験メモ(2020年)

誰? 大学では経済学を専攻していたが、大学院では情報科学の分野で研究をしたい人 社会人 プログラミング歴は約5年 受験の流れ 2020-04-19 オンラインでJapan Advanced Institute of Science and Technology(JAIST)の東京社会人コース説明会に参加した。 2020–04–22 関心のある研究室に受け入れが可能かを問うメールを送った。COVID-19のため、対面でなく …

3 min read

3 min read


May 2, 2020

Prove rev (rev L) = L in CafeOBJ

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…

Proof

5 min read

Prove rev (rev L) = L in CafeOBJ
Prove rev (rev L) = L in CafeOBJ
Proof

5 min read


Mar 14, 2020

RustでBFSする

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 を参照ください。

Rust

1 min read

Rust

1 min read

Takanori Ishibashi

Takanori Ishibashi

52 Followers

Software engineer

Help

Status

Writers

Blog

Careers

Privacy

Terms

About

Text to speech

Teams