UNIT 1:
Natural deduction - Rules for natural deduction
Soundness of propositional logic - Completeness of propositional logic
Soundness of propositional logic - Completeness of propositional logic
Propositional logic as a formal language
The meaning of logical connectives
UNIT 2:
Predicate logic - The need for a richer language
Predicate logic as a formal language – Terms
Alma - A software micromodel
Alma - A software micromodel
Existential second-order logic - Universal second-order logic
Formulas - Free and bound variables
Semantics of predicate logic – Models
Semantics of predicate logic – Models
Substitution - Proof theory of predicate logic
Substitution - Proof theory of predicate logic
Existential second-order logic - Universal second-order logic
UNIT 3:
The ferryman - Syntax of CTL
Adequate sets of CTL connectives
Important equivalences between LTL formulas
Linear-time temporal logic
Mutual exclusion - The NuSMV model checker
Practical patterns of specifications
Syntax of LTL - Semantics of LTL
Verification by model checking
Syntax of CTL Semantics of CTL
Important equivalences between CTL formulas, Adequate sets of CTL connectives
Model-checking algorithms
The expressive powers of LTL and CTL
UNIT 4:
Proof calculus for total correctness
Proof calculus for partial correctness: Proof rules
Modal logics and agents: Modes of truth
Program variables and logical variables
Partial and total correctness
Program verification - A core programming language
UNIT 5:
Representing subsets of the set of states
Binary decision diagrams : Representing Boolean functions
Propositional formulas and truth tables
Algorithms for reduced OBDDs The algorithm reduce, apply, restrict, exists
Representing the transition relation
Implementing the functions pre∃ and pre∀
Synthesizing OBDDs - A relational mucalculus
Syntax and semantics, Coding CTL models and specifications.
