# Formal methods reading list

**CORE list:**

Core Background: students are expected to know the following basic computer science and math background.

- Propositional Logic and Predicate Logic

For example, as covered in Chapters 1 and 2. from the book "Logic in Computer Science" by Huth and Ryan, covering:

propositional logic: natural deduction and proof theory, semantics, normal forms, satisfiability

predicate logic: syntax, substitution, proof theory, semantics, undecidability of satisfiability.

The CS498 on "Logic in Computer Science" or "Logical Systems" covers this (and more). - Basic automata theory and theory of computation:

Topics covered in the (undergrad) course CS373 or as in book M. Sipser, Introduction to the Theory of Computation, 2nd Edition,

or in book J. Hopcroft and J. Ullman, Introduction to Automata Theory. Languages and Computation, Addison-Wesley, 1979. - Basic theory of algorithms:

Topics as covered in (undergrad) course CS473, or as in book: Jon Kleinberg and Éva Tardos. Algorithm Design. Addison-Wesley, 2005. - Basic discrete mathemetics.

*As in*Discrete Mathematics and its Applications, 6 ed., by Kenneth H. Rosen

Articles in CORE reading list:

- An Axiomatic Basis of Computer Programming-- C.A.R. Hoare (Citeseer Link)

Courses that cover this: CS477, CS476 - Software Model Checking-- Jhala and Majumdar

Courses that cover this: CS477 - Abstract Interpretation: A Unified Lattice Model for Static Analysis Patrick Cousot and Radhia Cousot (an online version is available here)

(students might first want to read the paper "Construction of Abstract State Graphs using PVS" by Graf and Saidi, to see a concrete example of abstract interpretation in predicate abstraction)

Courses that cover this: CS477 - Automated Deduction for Verification - Natarajan Shankar

Courses that cover this: CS498 on "Logic in Computer Science" or "Logical Systems" and CS476.

**IN-DEPTH LIST:**

**Program Verification/Logic/Theorem Proving:**

- A Machine-Oriented Logic Based on the Resolution Principle -- J. A. Robinson

Courses that cover this: Resolution for prop logic is covered in CS498:Logic in Computer Science/Logical Systems;

also CS476. - Temporal and Modal Logic -- Allen Emerson (Citeseer link)

In Handbook of Theoretical Computer Science

Read Sections 1 to 5, and Section 7 of the chapter.

Courses that cover this: LTL is covered in CS498:Logic in Computer Science/Logical Systems; also in CS477. - Efficient Monitoring of Safety Properties \-\- Grigore Rosu (local link)

Int'l Journal on Software Tools for Technology Transfer, Vol. 6, No. 2, pp 158-173, 2004.

**Term rewriting:**

- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems - Gerard Huet

Courses that cover this: CS476 - Rewriting logic as a semantic framework for concurrency: a progress report - Jose Meseguer

Courses that cover this: CS476

**Abstract Interpretation and Model Checking**:

- Symbolic Model Checking -- Ken McMillan; Chapter 2, Pages 25--62:

Temporal logics and CTL; fixed-point characterization and model-checking using BDDs, - Visibly pushdown automata - R. Alur and P. Madhusudan (local link)
- On Statistical Model Checking of Stochastic Systems -- Koushik Sen, Mahesh Viswanathan, Gul Agha (local link)

Conf. on Computer Aided Verification (CAV), 2005.

**Concurrency:**

- Communication and Concurrency - Robin Milner (Prentice Hall)

Chapters 1,2,4.

Courses that cover this: CS524 - A foundation for Actor Computation - Gul Agha (Citeseer link)

Courses that cover this: CS524

**OPTIONAL SUPPLEMENTARY READING:**

The following books and papers are good sources that give alternate treatments of some of the topics above. Students may find these useful to understand some of the the above topics, as well as other topics not covered above.

- Assigning Meanings to Programs by Robert Floyd

In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of

Proceedings of Symposia on Applied Mathematics, pages19--32. American Mathematical Society, 1967

(An online link)

Read this to understand Hoare's paper better (Floyd's paper gives reasoning in terms of flow-charts and gives termination arguments,

and appeared just before Hoare's paper). - Calculus of Computation - Bradley and Manna

A good introduction to logic, SAT/SMT solving, decidable logics, and Hoare-style verification; available online. - Principles of Program Analysis - Nielson, Nielson, Hankin

Good source for static analysis techniques, abstract interpretation, and shape-analysis. *Axiomatic set theory.*

As in Jose Meseguer's notes on axiomatic set theory (chapters 1 through 11, omitting chapters 5,8,10 which are on case studies. This covers sets, induction, fixed-points and cardinality of sets).