Formal Specification and Verification

Prerequisite: Computer Science 130A-B; Computer Science 186.
Introduction to existing specification and verification systems, and the underlying theory and techniques of verifying the correctness of algorithms with respect to specifications. This subject can be considered as the combination of specification and verification techniques, programming language semantics and formal logic.