Efnisyfirlit

• Cover
• Half Title
• Title Page
• Copyright
• Contents
• Foreword to the first edition
• Preface to the second edition
• Acknowledgements
• 1. Propositional logic
• 1.1 Declarative sentences
• 1.2 Natural deduction
• 1.2.1 Rules for natural deduction
• 1.2.2 Derived rules
• 1.2.3 Natural deduction in summary
• 1.2.4 Provable equivalence
• 1.2.5 An aside: proof by contradiction
• 1.3 Propositional logic as a formal language
• 1.4 Semantics of propositional logic
• 1.4.1 The meaning of logical connectives
• 1.4.2 Mathematical induction
• 1.4.3 Soundness of propositional logic
• 1.4.4 Completeness of propositional logic
• 1.5 Normal forms
• 1.5.1 Semantic equivalence, satisfiability and validity
• 1.5.2 Conjunctive normal forms and validity
• 1.5.3 Horn clauses and satisfiability
• 1.6 SAT solvers
• 1.6.1 A linear solver
• 1.6.2 A cubic solver
• 1.7 Exercises
• 1.8 Bibliographic notes
• 2. Predicate logic
• 2.1 The need for a richer language
• 2.2 Predicate logic as a formal language
• 2.2.1 Terms
• 2.2.2 Formulas
• 2.2.3 Free and bound variables
• 2.2.4 Substitution
• 2.3 Proof theory of predicate logic
• 2.3.1 Natural deduction rules
• 2.3.2 Quantifier equivalences
• 2.4 Semantics of predicate logic
• 2.4.1 Models
• 2.4.2 Semantic entailment
• 2.4.3 The semantics of equality
• 2.5 Undecidability of predicate logic
• 2.6 Expressiveness of predicate logic
• 2.6.1 Existential second-order logic
• 2.6.2 Universal second-order logic
• 2.7 Micromodels of software
• 2.7.1 State machines
• 2.7.2 Alma – re-visited
• 2.7.3 A software micromodel
• 2.8 Exercises
• 2.9 Bibliographic notes
• 3. Verification by model checking
• 3.1 Motivation for verification
• 3.2 Linear-time temporal logic
• 3.2.1 Syntax of LTL
• 3.2.2 Semantics of LTL
• 3.2.3 Practical patterns of specifications
• 3.2.4 Important equivalences between LTL formulas
• 3.2.5 Adequate sets of connectives for LTL
• 3.3 Model checking: systems, tools, properties
• 3.3.1 Example: mutual exclusion
• 3.3.2 The NuSMV model checker
• 3.3.3 Running NuSMV
• 3.3.4 Mutual exclusion revisited
• 3.3.5 The ferryman
• 3.3.6 The alternating bit protocol
• 3.4 Branching-time logic
• 3.4.1 Syntax of CTL
• 3.4.2 Semantics of CTL
• 3.4.3 Practical patterns of specifications
• 3.4.4 Important equivalences between CTL formulas
• 3.4.5 Adequate sets of CTL connectives
• 3.5 CTL* and the expressive powers of LTL and CTL
• 3.5.1 Boolean combinations of temporal formulas in CTL
• 3.5.2 Past operators in LTL
• 3.6 Model-checking algorithms
• 3.6.1 The CTL model-checking algorithm
• 3.6.2 CTL model checking with fairness
• 3.6.3 The LTL model-checking algorithm
• 3.7 The fixed-point characterisation of CTL
• 3.7.1 Monotone functions
• 3.7.2 The correctness of SATEG
• 3.7.3 The correctness of SATEU
• 3.8 Exercises
• 3.9 Bibliographic notes
• 4. Program verification
• 4.1 Why should we specify and verify code?
• 4.2 A framework for software verification
• 4.2.1 A core programming language
• 4.2.2 Hoare triples
• 4.2.3 Partial and total correctness
• 4.2.4 Program variables and logical variables
• 4.3 Proof calculus for partial correctness
• 4.3.1 Proof rules
• 4.3.2 Proof tableaux
• 4.3.3 A case study: minimal-sum section
• 4.4 Proof calculus for total correctness
• 4.5 Programming by contract
• 4.6 Exercises
• 4.7 Bibliographic notes
• 5. Modal logics and agents
• 5.1 Modes of truth
• 5.2 Basic modal logic
• 5.2.1 Syntax
• 5.2.2 Semantics
• 5.3 Logic engineering
• 5.3.1 The stock of valid formulas
• 5.3.2 Important properties of the accessibility relation
• 5.3.3 Correspondence theory
• 5.3.4 Some modal logics
• 5.4 Natural deduction
• 5.5 Reasoning about knowledge in a multi-agent system
• 5.5.1 Some examples
• 5.5.2 The modal logic KT45n
• 5.5.3 Natural deduction for KT45n
• 5.5.4 Formalising the examples
• 5.6 Exercises
• 5.7 Bibliographic notes
• 6. Binary decision diagrams
• 6.1 Representing boolean functions
• 6.1.1 Propositional formulas and truth tables
• 6.1.2 Binary decision diagrams
• 6.1.3 Ordered BDDs
• 6.2 Algorithms for reduced OBDDs
• 6.2.1 The algorithm reduce
• 6.2.2 The algorithm apply
• 6.2.3 The algorithm restrict
• 6.2.4 The algorithm exists
• 6.2.5 Assessment of OBDDs
• 6.3 Symbolic model checking
• 6.3.1 Representing subsets of the set of states
• 6.3.2 Representing the transition relation
• 6.3.3 Implementing the functions pre∃ and pre∀
• 6.3.4 Synthesising OBDDs
• 6.4 A relational mu-calculus
• 6.4.1 Syntax and semantics
• 6.4.2 Coding CTL models and specifications
• 6.5 Exercises
• 6.6 Bibliographic notes
• Bibliography
• Index