Classifying and Solving Horn Clauses for Verification

Philipp Rümmer, Hossein Hojjat and Viktor Kuncak

プログラム検証の文脈で使われている Craig interpolation の変種たちを CHC solving を使って分類した論文（計算量などの性質についても少し議論されている）

技術的な結果としては各種 interpolation と各種 CHC の等価性や計算量の解析などあるものの、本論文の価値は interpolation のサーベイ論文としての面にあるのではないだろうか。いろいろな interpolation の変種たちが出典付きで載っていて、interpolation について網羅的に調べたり、特定の interpolation の導入の動機を知りたかったりしたときに使えそう。