Propositional logic: Declarative sentences - Natural deduction - Rules for natural deduction - Derived rules - Provable equivalence - Propositional logic as a formal language - The meaning of logical connectives - Mathematical induction - Soundness of propositional logic - Completeness of propositional logic - Normal forms - Semantics of propositional logic - Conjunctive normal forms and validity - Horn clauses and satisfiability - SAT solvers - A linear solver - A cubic solver.

Predicate logic - The need for a richer language - Predicate logic as a formal language – Terms – Formulas - Free and bound variables – Substitution - Proof theory of predicate logic - Natural deduction rules – Quantifier equivalences - Semantics of predicate logic – Models - Semantic entailment - The semantics of equality - Undecidability of predicate logic - Expressiveness of predicate logic - Existential second-order logic - Universal second-order logic – Micromodels of software - State machines – Alma - A software micromodel.

Verification by model checking - Motivation for verification - Linear-time temporal logic - Syntax of LTL - Semantics of LTL - Practical patterns of specifications - Important equivalences between LTL formulas - Adequate sets of connectives for LTL - mutual exclusion - The NuSMV model checker - The ferryman - Syntax of CTL - Semantics of CTL - Practical patterns of specifications - Important equivalences between CTL formulas - Adequate sets of CTL connectives – The expressive powers of LTL and CTL - Modelchecking algorithms - The fixed-point characterization of CTL.

Program verification - A core programming language - Hoare triples - Partial and total correctness - Program variables and logical variables - Proof calculus for partial correctness - Proof rules - Proof tableaux - Proof calculus for total correctness - Modal logics and agents - Modes of truth - Basic modal logic - Logic engineering - Natural deduction - Reasoning about knowledge in a multi-agent system.

Binary decision diagrams - Representing Boolean functions - Propositional formulas and truth tables - Binary decision diagrams - Ordered BDDs - Algorithms for reduced OBDDs - The algorithm reduce, apply, restrict, exists - Symbolic model checking - Representing subsets of the set of states - Representing the transition relation - Implementing the functions pre∃ and pre∀ - Synthesizing OBDDs - A relational mu-calculus - Syntax and semantics - Coding CTL models and specifications.