Verification of infinite-state systems by specialization of CLP programs