The goal of this course is to introduce students to some modern approaches that can
simplify the software development process. We will describe a number of program
checking techniques, explain their pros and cons, and discuss what else needs to be
done in order to make them fully applicable to real-life software systems.

In this lecture, we will cover some state-of-the-art techniques that check and detect
correctness properties of programs. We will particularly focus on lightweight tech-
niques that work at a push-of-a-button: those that are fully automatic and expect
very little input from users. Because these techniques do not depend on much user-
provided guidance and can be run without any user interactions, they can be easily
incorporated into a wide range of software development processes.

In this lecture, we will cover techniques for:

• Generating test cases exhaustively,
• Generating test cases randomly,
• Finding bugs in object-oriented programs,
• Summarizing programs’ behavior,
• Detecting invariants about programs.