Software Verification

Catalog description

This course will cover concepts, methods, and tools for formal verification of software. Software paradigms include object-oriented, functional and concurrent software. The course will cover software specification languages based upon set theory and various logics, and verification techniques that are code-based and model-based. Important topics include code contracts, weakest pre-conditions, invariants, termination, induction, model checking, and the use of modern tools for software verification. Adoption of verification methods in industry will also be surveyed. This course is dual-listed with CSE 549.