Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. Int. J. Softw. Tools Technol. Transf. 12(5): 319-335 (2010)