Automated Software Verification: Software Model Checking

Princeton University, Spring 2011, ELE/COS 580 (course website)

This course covers contemporary automated verification techniques for software. The focus is on the underlying techniques and algorithms rather than on using verification tools. The course is divided into two main parts: One covering model checking for finite state models (e.g., manual abstractions or UML state-charts), and a second part that shows how these techniques can be applied to infinite state programs by means of abstraction.