Automata-Theoretic Software Analysis, Caltech 2023-24, Winter Term

Course Material CS 118, TThu, 1:00-2:25pm, 121 Annenberg

Automata-Theoretic 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 property-based static source code analysis.

We discuss the theoretical basis 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 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, non-determinism, omega-regular properties, concurrent algorithms, storage methods, Bloom filters, temporal logic, language design, lexical analysis and parsing.

At the end of the course you should have a good insight into the theory and practice of automata-theoretic verification techniques, and the direction in which the research in this field is evolving. You should also be able to tackle complex real-world 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 self-paced work with the Spin and Cobra analysis tools (Linux or Mac based) is expected. Grading is based on take-home assignments and class participation. (You are expected to attend all lectures and ask questions.)

• All assignments require individual work.
• You may suggest reasonably challenging formal verification or software analysis tasks to replace any assignment.
• The first lecture is Tuesday January 9; the last will be Thursday March 7.
• Course assignments and additional materials will be posted on Canvas.

Lectures

• All lectures will be in person at 121 Annenberg. You are expected to attend, ask questions, start discussions, suggest problems.
• 20% of the course credit is based on your class participation.
• 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.
  Compile the tools from their sources (requires gcc or equivalent, yacc, lex etc) 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, gerard.holzmann [at] gmail.com, homepage

Teaching Assistant

Terry Huang, thhuang [at] caltech.edu

Background material (optional)

• Dijkstra's paper on guarded commands
• Hoare's paper on CSP
• Amir Pnueli's 1977 paper on temporal logic and model checking
• How many CPUs are there in a Mercedes S-class car? (50!)
• NIST report on economic impact of faulty software
• Standish survey of software projects
• Model Checking overview by Stephan Merz
• Wiki entry on formal verification
• IEEE Spectrum: Why software fails
• Wired: History's Worst Software Bugs
• CNN/Money: Prius hybrids dogged by software
• Computerworld: Buggy software costs $60B annually
• Embedded.com: Automotive industry software bugs
• ACM Paper on out-of-order execution on modern processors
• Spin model based on this paper, showing the bug in Peterson's mutual exclusion algorithm when executed on a modern processor
• Truth a thought provoking editorial published in 2008 in the Notices of the AMS.

Course Textbook (recommended)

• The Spin Model Checker: Primer and Reference Manual.
  Gerard Holzmann. Addison-Wesley, 2004.

Optional

• Principles of Spin,
  Moti Ben-Ari, Springer Verlag, Jan. 2008.
• Principles of Model Checking,
  Cristel Baier, Joost-Pieter Katoen, Kim Larsen, MIT Press, May 2008.
• Principles of concurrent and Distributed Programming,
  Moti Ben-Ari, Addison-Wesley, 2006, 2nd Edition, based on Spin.
• Model Checking,
  Ed Clarke, Orna Grumberg, and Doron Peled. MIT Press, 1999.
• Systems and Software Verification: Model-Checking 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, Addison-Wesley, 2000.
• Verification of reactive systems,
  Klaus Schneider, Springer-Verlag 2004.
• Formale Modelle der Softwareentwicklung (in German),
  Stephan Kleuker, Vieweg-Teubner Verlag, 2009. Covering Spin, Uppaal, and Petri Nets.

For more on mutual exclusion algorithms, and design of distributed algorithms in general, consider also:

• Algorithms for Mutual Exclusion, Michel Raynal, MIT Press, 1986.
• Distributed Algorithms and Protocols, Michel Raynal, Wiley&Sons, 1988.
• Topics in Distributed Algorithms, Gerard Tel, Cambridge Univ. Press, 1991.