CSI5380

Software Verification and Testing

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. Formerly CSE 538. Prerequisite: Student must have graduate standing.

CSE538

School of Egr. and Comp. Sci.