Automata-Theoretic Software Analysis, Caltech 2022-23, Winter Term

Course Material CS 118, TThu, 1:00-2:25pm, 106 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.

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, non-determinism, omega-regular 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 automata-theoretic verification techniques, and the direction in which the research in this field is evolving. You should then 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.

A fair amount of self-paced work with the Spin and Cobra analysis tools is expected. Grading is based on take-home assignments, some of which require the correct formalization of problem statements and the identification of logic abstractions that can render tool-based formal verification tractable.


Recommended Preparation


Teaching Assistant

Background material (optional)

Course Textbook (optional, but recommended)


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

Spin homepage