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 と各…