by Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken与えられた状態遷移系から、状態上の述語を頂点に持つ遷移系を構成する手法の提案。ならびに、状態上の遷移系の分析と述語上の遷移系の分析を、情報を交換しながら並…

by Aws Albarghouthi and Kenneth L. McMillan良い interpolant を計算するための手法の提案。 概要 Interpolant は SMT ソルバの証明から抽出することができるが、従来の DILL(T) を基盤とする SMT ソルバの返す証明（およびそこから抽出される interpolant…

by Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv and Sharon ShohamPropositional classical logic で記述された LTS の invariant 発見問題についての計算量や情報理論による解析。遷移関係 については black-box として扱い、Hoare triple が成立する…

by Daniel Neider and Ufuk Topcu有限状態オートマトンで表現された (safety) 無限ゲームをオートマトン学習で解くというもの。Winning set を記述するオートマトンを反例駆動で探す。なお本論文で扱っているゲームは通常の意味での games over pushdown gra…

by Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe and Ilya Sergey帰納法を用いた証明において帰納法の仮定を適切に強める（＝補題発見）ことが本質的な課題であることは広く知られているが、同様にプログラムの自動合成では適切な補…

by Md Sohel Ahmed, Fuyuki Ishikawa and Mahito Sugiyama機械学習の学習を行うコードのバグを発見するためのテスト手法。こういったコードの検証が重要であることは論を待たないが、挙動が入力に強く依存しているためテストが難しい。正しさの保証された「…

by Zhenng Wang and Michael O'Boyleコンパイラにおける最適化への機械学習の応用に関するサーベイ。はじめての accessible introduction を謳っていて、中身も良くまとまっている良いサーベイ。 概要 「新しい高度なプログラム変換」を機械学習で発見する話…

(Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo and Wei-Ngan Chin)Separation logic の symbolic heap の entailment problem を解くために、自動で補題発見をしようというもの。その方法は、補題が必要そうな場所に（解釈を定めない）述語変数を置き、述…

Philipp Rümmer, Hossein Hojjat and Viktor Kuncakプログラム検証の文脈で使われている Craig interpolation の変種たちを CHC solving を使って分類した論文（計算量などの性質についても少し議論されている）技術的な結果としては各種 interpolation と各…

僕の論文が小馬鹿にされているのを聞いて、むっとして反論を考えていたのだけど、冷静になって考えてみると、そうした反論は論文中に書かれているべきであり、また実際にいろいろと反省すべき点もあので、せっかくの機会に過去の論文を振り返り、反省を次の…

Swift の Array型の（書き換え可能な）変数の挙動が変だと、少し前に話題になっていたけれども、 var x = [1, 2, 3] : Arrayなんてやったら x の型は（OCaml風の記法で）int array ref 型なんですが、int array は int list ref とか int table ref みたいな…

手頃な演習問題のメモ。 を（空でない）有限集合とし を 上の正規言語の集合とする。この集合に部分集合関係によって順序集合となる：つまり について、 iff 。この順序について はCPOを成すか。証明または反例を与えよ。 この問題そのものがひっかけ問題っ…

トレース意味論とは、プログラムの意味を「実行したときに起きるイベントの列」として表現したものです。イベントとして何を考えるかは目的次第ですが、例えば「入出力」や「関数へ引数を渡す」などといったものが考えられます。以下でポイントになるのは、…

次のようなツイートを見かけたので、私なりの回答を。 初歩的な疑問だけど、untyped lambda calculusのbig-step semanticsってどう定義されるのだろう？計算が止まらない時にうまく定義できないように思うのだが。— yoriyuki (@yoriyuki) 2013, 11月 2 「計…