Abstract interpretation based verification of logic programs