Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. At the same time, the shift towa Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. At the same time, the shift towards internet-based distributed computing creates the need for individuals who are able to reason about sophisticated autonomous agent-oriented software acting on large networks. The second edition of this successful textbook addresses both those requirements, by continuing to provide an introduction to formal reasoning that is both relevant to the needs of modern computer science and rigorous enough for practical application. The presentation is clear and simple, with core material being described early in the book, and further technicalities introduced only where they are needed by the applications. A key feature is the full exposition of model-checking, and the new edition supports the most up-to-date versions of the tools NUSMV and Alloy. Improvements to the first edition have been made throughout, with extra and expanded sections on linear-time temporal logic model checking, SAT solvers, second-order logic, the Alloy specification tool, and programming by contract. The coverage of model-checking has been substantially updated. Further exercises have been added.
Logic in Computer Science: Modelling and Reasoning about Systems
Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. At the same time, the shift towa Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. At the same time, the shift towards internet-based distributed computing creates the need for individuals who are able to reason about sophisticated autonomous agent-oriented software acting on large networks. The second edition of this successful textbook addresses both those requirements, by continuing to provide an introduction to formal reasoning that is both relevant to the needs of modern computer science and rigorous enough for practical application. The presentation is clear and simple, with core material being described early in the book, and further technicalities introduced only where they are needed by the applications. A key feature is the full exposition of model-checking, and the new edition supports the most up-to-date versions of the tools NUSMV and Alloy. Improvements to the first edition have been made throughout, with extra and expanded sections on linear-time temporal logic model checking, SAT solvers, second-order logic, the Alloy specification tool, and programming by contract. The coverage of model-checking has been substantially updated. Further exercises have been added.
Compare
30 review for Logic in Computer Science: Modelling and Reasoning about Systems
Related products
The Turkish Letters of Ogier Ghiselin de Busbecq: A Biography
The Art of War: (Annotated with short biography)
Sir Elton: The Definitive Biography
Guernica: The Biography of a Twentieth-Century Icon
John Quincy Adams: A Life from Beginning to End (Biographies of US Presidents Book 6)
Kennedy: The Classic Biography
Geoffrey Chaucer
Ryan Finlayson –
Very good book for Verification module for SSE. I read the fourth chapter about program verification and it provided me with a great foundation for my exams :)
RomRomov –
Very well written. Gives required for formal verification background. Contains good excersizes for self study.
r –
I have not performed any model/program verification in practice, so it is impossible for me to determine to what extent this book provides a sufficient basis for such a task. I have also not read the book from cover to cover. Still, there is a lot of interesting and/or important theoretical material here. Some keywords: propositional logic, predicate logic, modal logic, temporal logic, Hoare logic (for program verification), natural deduction, Kripke semantics, binary decision diagrams and metal I have not performed any model/program verification in practice, so it is impossible for me to determine to what extent this book provides a sufficient basis for such a task. I have also not read the book from cover to cover. Still, there is a lot of interesting and/or important theoretical material here. Some keywords: propositional logic, predicate logic, modal logic, temporal logic, Hoare logic (for program verification), natural deduction, Kripke semantics, binary decision diagrams and metalogical discussions (soundness, completeness, decidability, etc.). While many metalogical proofs are omitted, it contains some nice ones. One example is the proof for the undecidability of predicate logic, in which it is demonstrated that the undecidable Post correspondence problem (for which the undecidability is not itself proven) can be expressed as a satisfiability problem. Most of the formal language in this book is also explained in natural language, making it relatively accessible.
Ushan –
A very brief overview of the applications of logic in computer science. It begins with the discussion of propositional logic, giving two constraint-based algorithms for solving the satisfiability problem, called "linear" and "cubic" (I don't get it - how can an NP-complete problem have a cubic algorithm, unless P=NP? This book doesn't look like an artefact from another planet or the future where P has been proven to equal NP), and predicate logic. It then gives an introduction to temporal logic, A very brief overview of the applications of logic in computer science. It begins with the discussion of propositional logic, giving two constraint-based algorithms for solving the satisfiability problem, called "linear" and "cubic" (I don't get it - how can an NP-complete problem have a cubic algorithm, unless P=NP? This book doesn't look like an artefact from another planet or the future where P has been proven to equal NP), and predicate logic. It then gives an introduction to temporal logic, illustrated by the wolf-goat-cabbage problem, modal logic, illustrated by the wise-men-and-hats problem, and discusses an optimized data structure for instances of SAT. Each chapter is too brief to be useful; fortunately, there is a further reading section in each chapter; unfortunately, it does not justify the price of the book.
Jiaming Jiang –
It gives a clear explanation about almost all the basic logics you need to know in the area of computer science, such as propositional logic, first-order logic, temporal logic and some modal logic. A great book on the introduction of logics.
Loke Mani –
Requires sure footing in abstract thinking and mathematical notation. Very thorough and shows not just how but why and what for. A very good introduction on an academic level.
Henk Poley –
Very reasonable book, lots of exercises.
Tom Duckering –
Larenopfer –
Burak –
Andrei Barbu –
Faizan –
Raul –
Vaira Selvakani –
Parlabane –
Joakim Bennedich –
Mattias Lundell –
Guillermo Garza –
Mike –
Ross Sponholtz –
Sreyas –
Matthias Moulin –
Dimitris –
Robert Antonio –
Julia –
Subhajit Das –
Jay –
Catherine –
Daniel –
Jacob –