1 Introduction. - 1. 1 Concurrent Programs. - 1. 2 Communication and Synchronization. - 1. 3 Understanding Concurrent Programs. - 1. 4 A Preview. - Historical Notes for Chapter 1. - Exercises for Chapter 1. - 2 Formal Logic. - 2. 1 Formal Logical Systems. - 2. 2 Propositional Logic. - 2. 3 A Predicate Logic. - 2. 4 Safety and Liveness Revisited. - Historical Notes for Chapter 2. - Exercises for Chapter 2. - 3 Temporal Logic. - 3. 1 Informal Preview. - 3. 2 Syntax and Meaning of Formulas. - 3. 3 Axioms and Inference Rules. - 3. 4 Temporal Logic Applications. - 3. 5 About Modal Logics. - Historical Notes for Chapter 3. - Exercises for Chapter 3. - 4 Notation and Logic for Sequential Programming. - 4. 1 Notation for Sequential Programs. - 4. 2 Reasoning About Program States. - 4. 3 Proof Outline Logic. - 4. 4 Assignment to Composite Variables. - 4. 5 A Predicate Transformer. - Historical Notes for Chapter 4. - Exercises for Chapter 4. - 5 Concurrency and Interference. - 5. 1 Specifying Concurrency. - 5. 2 Control Predicate Axioms. - 5. 3 Interference Freedom. - 5. 4 Hiding Control Predicates in Derived Terms. - 5. 5 Synchronously Altered and Shared Assertions. - 5. 6 Specifying Synchronization. - 5. 7 Synchronization and Interference. - Historical Notes for Chapter 5. - Exercises for Chapter 5. - 6 Safety Properties: Invariance. - 6. 1 Invariance Properties. - 6. 2 Verifying Invariance Properties. - 6. 3 Exclusion of Configurations. - 6. 4 Direct Use of Proof Outlines. - 6. 5 Developing Programs for Invariance Properties. - Historical Notes for Chapter 6. - Exercises for Chapter 6. - 7 Safety Properties with Past Terms. - 7. 1 Historical Safety Properties. - 7. 2 Past Extensions to Predicate Logic. - 7. 3 Verifying Historical Safety Properties. - 7. 4 Developing Programs for Historical Safety Properties. - 7. 5 Auxiliary Variables. - 7. 6 Some Cautions. - Historical Notes for Chapter 7. - Exercises for Chapter 7. - 8 Verifying Arbitrary Temporal Logic Properties. - 8. 1 S-Temporal Logic Revisited. - 8. 2 Unless Properties and Derivatives. - 8. 3 Fairness Assumptions. - 8. 4 Reasoning from Fairness Assumptions. - 8. 5 Helpful Actions and Eventualities. - 8. 6 Liveness for Mutual Exclusion. - Historical Notes for Chapter 8. - Exercises for Chapter 8. - 9 Programming with Fine-Grained Atomic Actions. - 9. 1 Pretending Atomicity. - 9. 2 Translation-Independent Reasoning. - 9. 3 Implementing Condition Synchronization. - 9. 4 Programming with the Subset. - 9. 5 Synchronization and Interference Revisited. - 9. 6 Interlock Instructions. - 9. 7 Example: Barrier Synchronization. - Historical Notes for Chapter 9. - Exercises for Chapter 9. - 10 Semaphores Locks and Conditional Critical Regions. - 10. 1 Semaphores. - 10. 2 Change of Variable to use Semaphores. - 10. 3 Binary Semaphores and Locks. - 10. 4 Split Binary Semaphore Method. - 10. 5 Conditional Critical Regions. - Historical Notes for Chapter 10. - Exercises for Chapter 10. - 11 Message Passing and Distributed Programming. - 11. 1 Asynchronous Message-Passing. - 11. 2 Synchronous Message-Passing. - 11. 3 Derivation of Distributed Programs. - 11. 4 Shared-Variable Representations. - Historical Notes for Chapter 11. - Exercises for Chapter 11. - 12 Putting It Together. - 12. 1 On Languages. - 12. 2 Principles for Verifying Safety and Liveness Properties. - 12. 3 Proofs Only Increase Confidence. - 12. 4 A Tool and Applications. - Historical Notes for Chapter 12. - References. Language: English