This textbook provides a thorough structured introduction to program verification. By covering both sequential and parallel programming, the authors show how these techniques may be used to prove the correctness of a wide variety of programs and they provide a number of demonstrations using case studies. Students coming to this subject for the first time will find this an ideal first course.