Formal methods reading list

CORE list:

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

  1. 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).
  2. 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.
  3. 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.
  4. Basic discrete mathemetics.
       As in Discrete Mathematics and its Applications, 6 ed., by Kenneth H. Rosen

Articles in CORE reading list:


IN-DEPTH LIST:

Program Verification/Logic/Theorem Proving:

Term rewriting:

Abstract Interpretation and Model Checking:

Concurrency:


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.

  1. 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).
  2. Calculus of Computation - Bradley and Manna
    A good introduction to logic, SAT/SMT solving, decidable logics, and Hoare-style verification; available online.
  3. Principles of Program Analysis - Nielson, Nielson, Hankin
    Good source for static analysis techniques, abstract interpretation, and shape-analysis.
  4. 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).

Theme by Danetsoft and Danang Probo Sayekti inspired by Maksimer