Overview

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]

01.05         Holiday

08.05         Alloy [slides] [exercise] -- bring your laptops

15.05         Alloy engine [slides]

22.05         Dynamic systems in Alloy [slides] [exercise] -- bring your laptops

29.05         Holiday

05.06         Bounded Verification by Jalloy [slides]

12.06         Bounded Verification by JForge [slides] -- bring your laptops

19.06         Holiday

26.06         Bounded Verification by Incremental analysis, ESC/Java, Houdini [slides]

03.07         Invariant Generation by Daikon [slides] [exercises] -- bring your laptops

10.07         Specification Inference [slides]

17.07         CEGAR-based specification extraction [slides]