{A Computational Logic-Based Approach to Verification of IT Systems}