Propositional logic: Declarative sentences-Natural deduction-Ruies for natural doo Derived rules-Provable equivalence - Propositional logic as a formal language-The meaning of logical connectives - Mathematical induction-Soundness of propositional logic Completenem of propositional logic Normal forms Semantics of propositional logic-Conjunctive sormal 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 Formalas - Free and bound variables-Substitution Proof theory of predicate logie Natural deduction rules-Quantifier equivalences Semantics of predicate legic-Models- Semantic entailment The semantics of equality Undecidability of predicate logic Expressiveness of prediente 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 Syntas of LTL. Semantics of LTL-Practical patterns of specifications-Important equivalences between LTL. formulas - Adequate sets of connectives for LTL-matual exclusion-The NuSMV model checker The ferryman Syntax of CTL Somantics of CTL Practical patterns of specifications-Important equivalences between CTL formulas-Adequate sets of CTL connectives The expressive powers of LTL and CTL Model-checking algorithms The fisedpoint 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 tablemax Proof calculus for total correctness - Modal logics and agents-Modes of truth-Basic modal logic-Logic engineering-Natural deduction-Reasoning about knowledge a multi-agent system

Binary decision diagrams - Representing Hoolean functions - Propositional formulas and truth tables - Binary decision diagrams Ordered BDDsAlgorithms 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 prell and prov - Synthesizing OBDDs - A relational mo-calculus-Syntax and semantics-Coding CTL models and specifications.