AutomataTheoretic Software Analysis, Caltech 202122, Winter Term
Course Material CS 118, TThu, 1:002:25pm, online and 106 Annenberg
AutomataTheoretic Software Analysis
An introduction to the use of automata theory in the formal analysis of both
concurrent and sequentially executing software systems. The course covers
the use of logic model checking with linear temporal logic and interactive
techniques for propertybased static source code analysis.
The course covers the theoretical basis for the use of logic model checking
techniques, as used in the Spin model checker.
More broadly, we cover the use of finite automata in the analysis, e.g. of
security vulnerabilities,
of software systems, as for instance implemented in the
Cobra static source code analysis tool.
We'll briefly also dip into efficient techniques for performing runtime
monitoring of executing systems.
The course covers a range of foundational CS topics,
including the use of hash tables, search methods, graph theory, automata theory,
nondeterminism, omegaregular properties, concurrent algorithms, storage methods,
Bloom filters, temporal logic, user interfaces, language design, lexical analysis
and parsing.
At the end of the course you should have a good insight into the
theory and practice of automatatheoretic verification techniques, and the
direction in which the research in this field is evolving.
You should then also be able to tackle complex realworld verification problems for
software systems involving concurrency.
Course materials, including assignments and additional tools, will likely be
maintained on Canvas.
If you're registered for the class, you'll receive an invitation to join.
Assignments:
A fair amount of selfpaced work
with the Spin and Cobra analysis tools is expected.
Grading is based on takehome assignments, some of which
require the correct formalization of problem statements and
the identification of logic abstractions that can render
toolbased formal verification tractable.

All assignments are require individual work.

You may suggest reasonably challenging formal verification or
software analysis tasks to replace any assignment.
 The first lecture is Tuesday January 4; the last will be Tuesday March 8.
 Course assignments and additional materials will be posted on Canvas.
Lectures
 Most lectures (including the first week) will be online  if possible, a few will be in person at 106 Annenberg.
 You are expected to attend all lectures, ask questions, start discussions, suggest problems.
 Part of the course credit is based on your class participation (asking questions, providing feedback).
 Grading is by letter grade.
Recommended Preparation
 In the week before the course starts, install the most recent versions of Spin and Cobra on your system from github.
DCompile the tools from their sources (requires gcc or equivalent) and
install them on your system.
 Install a recent version of tcl/tk and graphiz/dot on your system.
 Ubuntu/Linux is preferred, but both Mac and Windows/Cygwin environments also work fine.
Instructor
 Gerard J. Holzmann, gholzmann [at] acm.org, homepage
Teaching Assistant
 Ethan Eason, eeason [at] caltech.edu
Background material (optional)
Course Textbook (optional, but recommended)
Optional:

Principles of Spin,
Moti BenAri, Springer Verlag, Jan. 2008.

Principles of Model Checking,
Cristel Baier, JoostPieter Katoen, Kim Larsen, MIT Press, May 2008.

Principles of concurrent and Distributed Programming,
Moti BenAri, AddisonWesley, 2006, 2nd Edition, based on Spin.

Model Checking,
Ed Clarke, Orna Grumberg, and Doron Peled. MIT Press, 1999.

Systems and Software Verification: ModelChecking Techniques and Tools,
Beatrice Berard, Michel Bidoit, Alain Finkel, et al, Springer Verlag, 2001.

Logic in Computer Science: Modelling and Reasoning about Systems,
Michael Huth and Mark Ryan, Cambridge Univ. Press, 1999.

Introduction to Automata Theory, Languages, and Computation (2nd Edition),
John Hopcroft, Rajeev Motwani, Jeff Ullman, AddisonWesley, 2000.

Verification of reactive systems,
Klaus Schneider, SpringerVerlag 2004.

Formale Modelle der Softwareentwicklung (in German),
Stephan Kleuker, ViewegTeubner Verlag, 2009.
Covering Spin, Uppaal, and Petri Nets.
For more on mutual exclusion algorithms, and design of distributed algorithms
in general, consider also:
Spin homepage