CS 5110 - Software Verification and Analysis

The main goal of the course is to teach students how to rigorously verify and analyze (complex) software systems. We will study theoretical foundations underlying this task, and solve exercises and homework assignments based around actually proving example programs correct. We will also explore practical techniques behind popular verification and analysis tools, such as systematic test generation, symbolic execution, and static analysis. Students completing the course will gain a solid understanding of practical design, specification, and verification techniques and the underlying theory. Furthermore, students will leave with significant hands-on experience.