{Verification from Declarative Specifications Using Logic Programming}