CSE 538 Software Verification and Testing
(4 credits)
Description:
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 re used:
SPARK (Static Analysis, Verification), and STAD, System for Testing and
Debugging, for static analysis and testing.
Prerequisites: Graduate standing.