verifastに関するmasterqのブックマーク (22)
-
masterq 2022/10/22
-
-
-
-
-
-
-
-
Streams and parsers
The first extension provided by Camlp4 is streams and parsers. A stream is a value of the abstract type 'a Stream.t. It is like a list but where only the first element is available: to read the second element you have to remove the first one from the stream. A parser is a function of type 'a Stream.t -> 'b which makes a kind of pattern matching inside a stream. A first way to create a stream is to
-
静的コード解析の会#6で発表してきた - ::Eldesh a b = LEFT a | RIGHT b
静的コード解析の会#6でVeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…) 前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。 が、今回の発表では多重集合、整礎関係、実際の処理系で検査できるコードについての説明まで入れることが出来たので、これで一通りの内容を盛り込めたと思います(ただしシーケンシャルなプログラムに限る…)。 参照している論文はModular termination verificationです。 (多分)怪しげな記述や展開のよく分からないページがありますが、がんばって作ったので興味がある人は是非眺めてみて下さい。 個人的なおすすめはStatic Recursionパターンの検証方法のあたり(資料の末尾の方)です。 会場からは、 処理系が(もっと)がんばれ 発表の構成が悪い(直接そうは言われてないけど) とい
-
-
-
-
VeriFast Termination Checking Introduction(α)
静的コード解析の会 第2回 (https://metasepi.connpass.com/event/50450/) で発表した資料です。 VeriFastによるC(およびJava)言語の停止性証明に関する解説を行っています。停止性検査を行う理論的背景を説明し、これを行う際にVeriFastの採る大ま…
-
-
-
-
-
-
GitHub - verifast/verifast: Research prototype tool for modular formal verification of C and Java programs
By Bart Jacobs*, Jan Smans*, and Frank Piessens*, with contributions by Pieter Agten*, Cedric Cuypers*, Lieven Desmet*, Niels Mommen*, Jan Tobias Muehlberg*, Willem Penninckx*, Pieter Philippaerts*, Nima Rahimi Foroushaani*, Amin Timany*, Thomas Van Eyck*, Gijs Vanspauwen*, Frédéric Vogels*, and external contributors * imec-DistriNet research group, Department of Computer Science, KU Leuven - Univ
公式Twitter
- @HatenaBookmark
リリース、障害情報などのサービスのお知らせ
- @hatebu
最新の人気エントリーの配信
キーボードショートカット一覧
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
