Project Overview

Scientific foundations for software engineering depend on the use of precise, abstract models and
logics for characterizing and reasoning about properties of software systems. A number of basic
models and logics over time have proven to be particularly important and pervasive in the
development of software systems. This course is concerned with that body of knowledge. It
considers many of the standard models for representing sequential and concurrent systems, such
as state machines, algebras and traces. It shows how you can use different logics to specify
properties of software systems, such as functional correctness, deadlock freedom, and internal
consistency. Concepts such as composition mechanisms, abstraction relations, invariants, nondeterminism, and inductive and denotational descriptions are recurrent themes throughout the
By the end of the course, you should be able to understand the strengths and weaknesses of certain
models and logics, including state machines, algebraic and trace models, probabilistic models, and
temporal logics. You should be able to apply this understanding to select and describe abstract
formal models for certain classes of systems. Further, you should be able to reason formally about
the important properties of modeled systems.


David Garlan, Eugene Kang

Relevant Links

Models of Software Systems