Logic in Computer Science: Modelling and Reasoning About Systems

by Michael Huth, Mark Ryan

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.

Genres: Computer Science, Logic, Mathematics, Textbooks, Nonfiction, Programming, Reference

447 pages, Paperback

First published December 28, 1999

About the author

Librarian Note: There is more than one author in the Goodreads database with this name.

Reviews

[Ryan · Rating 5 out of 5]

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 :)

[Lacie · Rating 4 out of 5]

I had to read this for class, but it was actually surprisingly palatable. When I couldn’t understand the instructors or follow their logic in class, this book really laid things out in a way that was intuitive to understand. The caveat is, I’ve been working in the computing industry for over a decade now, so I have familiarity with the coding concepts and logic issues that the book is trying to address. In my younger less knowledgeable days, I doubt this would have been an easy read.

Basically, this book tackles the problem of trying to rigorously validate a program’s correctness. Imagine writing spaghetti code in such a way that you lose the ability to resolve all the possible outputs or inputs. Shit keeps breaking, or worse, hacked by someone who was able to find a system state that you didn’t consider. THAT’s basically what this topic is trying to fix, in a nutshell. It is an abstraction of the coding process — a way of thinking about your approach to code — and explains how to think logically to prove that your program works as expected. (Obviously, in practice, environmental factors like an overheating computer can cause issues with your rigorously thought-out and proven computation, but that is a whole other topic in itself.)

Anyway, as a computer/network security practitioner, I kinda dig the treatment this book gave to the topic. There’s a lot of takeaways here.

I feel like I should also give extra brownie points for the old-school font and formatting. Have you ever read science/math textbooks from the 1950s? They’re so much easier to follow than a lot of textbooks these days. I’d say this book had that similar old school feel to it. I loved that.

[RomRomov · Rating 5 out of 5]

Very well written. Gives required for formal verification background. Contains good excersizes for self study.

[Ushan · Rating 3 out of 5]

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 · Rating 4 out of 5]

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.

[Henk Poley · Rating 4 out of 5]

Very reasonable book, lots of exercises.

[Loke · Rating 4 out of 5]

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.