CSE 538 - Software Verification and Testing

(4 credits)

The course consists of three main parts: Formal Verification (proofs of correctness), Static Program Analysis (detection of program anomalies, explanatory analysis, static debugging) and Dynamic Program Analysis (testing and debugging), the latter two representing software engineering approach to software verification. Most of the course consists of lectures by the instructor and discussions of the assignments. If the size of the class is relatively small, a seminar could be required in lieu of an assignment. Two software tools are used: SPARK (Static Analysis, Verification), and STAD (System for Testing and Debugging) for static analysis and testing.

Prerequisite(s): Student must have graduate standing.

Course revisions made after the Graduate Catalog publication date will be posted in the Graduate Catalog Addendum.