One of the leitmotifs of writing the first edition of our book was the observation that most logics used in the design, specification and verification of computer systems fundamentally deal with a satisfaction relation M |= phi where M is some sort of situation or model of a system, and phi is a specification, a formula of that logic, expressing what should be true in situation M. At the heart of this set-up is that one can often specify and implement algorithms for computing |=. We developed this theme for propositional, first-order, temporal, modal, and program logics. Based on the encouraging feedback received from five continents we are pleased to hereby present the second edition of this text which means to preserve and improve on the original intent of the first edition.
What's New and What's Gone
Chapter 1 now discusses the design, correctness, and complexity of a SAT solver (a marking algorithm similar to Stalmarck's method for full propositional logic.
Chapter 2 now contains basic results from model theory (Compactness Theorem and Loewenheim-Skolem Theorem); a section on the transitive closure and the expressiveness of existential and universal second-order logic; and a section on the use of the object modelling language Alloy and its analyzer for specifying and exploring under-specified first-order logic models with respect to properties written in first-order logic with transitive closure. The Alloy language is executable which makes such exploration interactive and formal.
Chapter 3 has been completely re-structured. It now begins with a discussion of linear-time temporal logic; features the open-source NuSMV model-checking tool throughout; and includes a discussion on planning problems, more material on the expressiveness of temporal logics, and new modelling examples.
Chapter 4 contains more material on total correctness proofs and a new section on the programming-by-contract paradigm of verifying program correctness.
Chapters 5 and 6 have also been revised, with many small alterations and corrections.