Jinji Yang, Kaile Su, Qingliang Chen: Improving Encoding Efficiency for Bounded Model Checking. TASE 2008: 31-38