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

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

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