Introduction and Foundational Theory

 Type Systems: A Foundation for Reliable Computing Robert Harper
We will introduce type systems, the most basic mechanism for static verification of program behavior and a solid foundation for reliable programming. Students will learn how to define type systems for simple programming languages and how to prove that their type systems are sound. We will also explore the connections between type systems and constructive logic. We will consider systems of natural deduction, sequent calculus, term assignment, normalization, and operational interpretations of proof terms. Materials will be drawn from the first half of the course Constructive Logic at Carnegie Mellon. These lectures serve as introductory material for the more advanced topics on type checking, static safety, logic and program verification.

 An Introduction to Model Checking Orna Kupferman
Finite automata on infinite objects were first introduced in the 60's, and were the key to the solution of several fundamental decision problems in mathematics and logic. Today, automata on infinite objects are used for specification and verification of nonterminating programs. The idea is simple: when a program is defined with respect to a finite set P of propositions, each of the program's states can be associated with a set of propositions that hold in this state. Then, each of the program's computations induces an infinite word over the alphabet 2P, and the program itself induces a language of infinite words over this alphabet. This language can be defined by an automaton. Similarly, a specification for a program, which describes all the allowed computations, can be viewed as a language of infinite words over 2P, and can therefore be defined by an automaton. In the automata-theoretic approach to verification, we reduce questions about programs and their specifications to questions about automata. More specifically, questions such as satisfiability of specifications and correctness of programs with respect to their specifications are reduced to questions such as nonemptiness and language containment. The automata-theoretic approach separates the logical and the combinatorial aspects of reasoning about programs. The translation of specifications to automata handles the logic and shifts all the combinatorial difficulties to automata-theoretic problems. We will define automata on infinite words, study some of their properties, and see how they are used in formal verification.

 Logics for Dynamic Data Structures Uday S. Reddy
Dynamic data structures are those allocated dynamically and addressed via pointers or references. They include data structures like linked lists, trees and graphs, and all objects in object-oriented languages like Java. Traditional Hoare Logic-based reasoning does not work well for such structures because it does not capture modularity. Great strides on this problem have been made in recent years through the development of Separation Logic by Reynolds, O'Hearn and others, and it is an active research area. This course covers all aspects of Separation Logic at its present stage, including reasoning about data structures, ownership representation, concurrency and automatic verification.