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,
- Designing feedback loops for analyzing large programs.