No label defined (Q4953875)

This monograph is an unusual, inspiring and remarkable book. It not only gives a careful introduction to the logical frameworks which are used in modelling and reasoning about computer systems, with a long list of examples and exercises, but one can find in it all the material which is suitable for undergraduate and beginning graduate students in computer science and electrical engineering who will profit by using it in their professional activities in the near future. The material in this book is elegantly presented at a level that is accessible to undergraduate and beginning graduate students. The book is supported by a WWW page which contains a list of errata, text files for all the program code, and all the figures. It contains also an interactive tutor based on multiple-choice questions. There are also details of how to obtain the solutions to exercises in this book which are marked with a *. The book consists of six chapters. Chapter 1 contains a complete presentation of a deduction-style proof system for propositional logics, a section on propositional logic as a formal language, and the semantics of propositional logic. In Chapter 2 the authors define and study predicate logic as a formal language and its semantics, introduce a deduction-style proof system for predicate logic, and present Church's theorem on the undecidability of satisfaction in predicate logic. Chapter 3 introduces model checking, a state-of- the-art technique in verifying concurrent systems. Chapter 4 contains program verification by discussing deductive reasoning about imperative programs. Chapter 5 discusses modal logics and agents. Finally, Chapter 6 introduces binary decision diagrams, which are a data structure for Boolean functions.