| |
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.
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.
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.
|
|
