“Proving properties for Bounded Model Checking” 2006.