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 techniques 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,
• Generating test cases by symbolic execution,
• Generating test cases by concolic execution.