|
Schedule | |||||||||||||
|
|
- DESCRIPTION:
-
Debugging programs can be a tedious task, since bugs can hide everywhere: in the data, the code, or in the decisions of how to combine them to form objects. Even after hours of testing and debugging, familiar and tricky questions arise: "have we tested enough, are there still bugs, or does the program work correctly now?" A fundamental approach to address these questions once and for all is to verify the correct functioning of the program with respect to its specification. One of the verification challenges for many current programming languages (Java,C++,Python,...), is that they have objects combining data (information) and code (behavior).
For handling data during verification we need to understand corresponding theories and decision procedures, e.g., for (fragments of) linear integer arithmetic, rational/real arithmetic, arrays and the like. For code, we need to understand its effect and the impact of decisions in control structures. The analysis becomes particularly intricate for object-oriented programs, where the dynamic type of the data determines which code to execute, which, in turn, determines the transformation on the data, which may finally affect code execution at a later point in time ... Ultimately, data and code become interdependent in the presence of aliasing of object references.
This class will provide you with logic-based techniques for verifying object-oriented programs, their data and code. At the same time, the course provides insight on various decision procedures for theories relevant in the domain of program verification. Decision procedures can be used to decide, e.g., whether a property is true in a suitable theory/interpretation of first-order logic. These theories and their combination are of independent interest and have applications in many other areas, including, e.g., hybrid systems analysis.
- OBJECTIVES:
- You will learn how to verify object-oriented Java programs. You will learn to understand techniques for analyzing various features of common object-oriented programming languages. In addition, the course will provide you with a background on relevant decision procedures and theories.
- PREREQUISITES:
- Understanding of Java or similar object-oriented programming languages (C++,...) is essential. Basic knowledge in logic will be important (a short introduction will be provided in class).
- METHOD OF EVALUATION:
-
Grading will be based on a set of homework assignments, including hands-on analysis experience, midterm exam, and a final project (30% Homework, 15% Midterm, 55% Project).
The project component will be one large or several small projects related to object-oriented program verification or decision procedures. It can include practical programming, applications, the development of theory, or the presentation of work in seminar style. - TOPICS TO BE COVERED:
-
- Object-oriented Programs and Bugs
- Propositional Logic
- First-order Logic
- Equational Decisions
- Decision Procedures for Linear Arithmetic
- Dynamic Logic for Imperative Programs
- Arithmetic Domains
- Fourier-Motzkin Decision Procedures
- Static Typing
- Dynamic Logic for Object-oriented Programs
- Ferrante-Rackoff Decision Procedures
- Presburger Arithmetic
- Dynamic Instantiation and Dynamic Typing
- Pointer Aliasing
- Gröbner Bases and the Nullstellensatz
- Exception Handling
- Cohen-Hörmander Decisions
- Procedure Calls
- Dynamic Method Binding and Inheritance
- Positivstellensatz
- Real Nullstellensatz
- Nelson-Oppen Theory Combination
- Time permitting: Java Modeling Language JML
- Time permitting: Proof Theory of Object-oriented Software
- Time permitting: Abstraction Refinement
- Time permitting: Craig Interpolation
- Time permitting: Theory of Arrays
- Time permitting: Ω-procedure