A Counterexample-Guided Interpolant Generation Algorithm for SAT-Based Model Checking IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2014 2014 作者：Cheng-Yin Wu, Chi-An Wu, Chien-Yu Lai, Chung-Yang Ric Huang
