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 cover a number of recently-developed techniques for checking functionality of programs. That is, they are alternatives to software testing. 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.
The lecture will cover the following topics:
• Finding bugs in object-oriented programs,
• Summarizing programs’ behaviors,
• Detecting invariants about programs,
• Feedback loops
Schedule and Slides
24.04 Introduction [slides]
15.05 Alloy engine [slides]
05.06 Bounded Verification by Jalloy [slides]
12.06 Bounded Verification by JForge [slides] -- bring your laptops
26.06 Bounded Verification by Incremental analysis, ESC/Java, Houdini [slides]
10.07 Specification Inference [slides]
17.07 CEGAR-based specification extraction [slides]