Foundations of Program Verification