@techreport{oai:ipsj.ixsq.nii.ac.jp:00209545,
 author = {喜多村, 卓 and 上原, 哲太郎},
 issue = {8},
 month = {Feb},
 note = {IoT 製品においては，製品出荷後のバグ修正が困難なシステムなど，開発時点でバグがあってはならないシステムが存在する．このようなシステムは，プログラム開発時点で堅牢なプログラムであることは重要である．プログラムの堅牢性を保証する開発手法として形式手法が提案されているが，実際の開発現場では普及しているとは言えない．本研究では，形式手法普及の阻害要因を明らかにする目的で，プログラム検証用言語である F*言語を用いて堅牢なシステムであることが求められる MQTT パケットパーサを開発し，その過程で明らかになった課題を整理するとともに，安全性評価を行った．},
 title = {F<sup>*</sup>言語によるMQTTパケットパーサの開発と安全性評価},
 year = {2021}
}