A computational logic-based approach to verification of IT systems