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 が成立する…