[B! japanese][verifast] masterqのブックマーク

masterq id:masterq

japaneseとverifastに関するmasterqのブックマーク (2)

静的コード解析の会#6で発表してきた - ::Eldesh a b = LEFT a | RIGHT b
静的コード解析の会#6でVeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…) 前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。が、今回の発表では多重集合、整礎関係、実際の処理系で検査できるコードについての説明まで入れることが出来たので、これで一通りの内容を盛り込めたと思います(ただしシーケンシャルなプログラムに限る…)。参照している論文はModular termination verificationです。 (多分)怪しげな記述や展開のよく分からないページがありますが、がんばって作ったので興味がある人は是非眺めてみて下さい。個人的なおすすめはStatic Recursionパターンの検証方法のあたり(資料の末尾の方)です。会場からは、処理系が(もっと)がんばれ発表の構成が悪い(直接そうは言われてないけど) とい
masterq 2018/01/26
verifast

japanese

termination

verify
リンク
VeriFast Termination Checking Introduction(α)
静的コード解析の会第2回 (https://metasepi.connpass.com/event/50450/) で発表した資料です。 VeriFastによるC(およびJava)言語の停止性証明に関する解説を行っています。停止性検査を行う理論的背景を説明し、これを行う際にVeriFastの採る大まかな方針と検証のアイデアを説明しています。
masterq 2017/04/29
verifast

presentation

slide

japanese
リンク
1