The second edition of this successful textbook continues to provide a clear introduction to formal reasoning relevant to the needs of modern computer science and sufficiently exacting for practical applications. Improvements have been made throughout with many new and expanded text sections. The coverage of model-checking has been substantially updated and additional exercises are included. Internet support includes worked solutions for teacher exercises and model solutions to some student exercises. First Edition Hb (2000): 0-521-65200-6 First Edition Pb (2000): 0-521-65602-8
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 :)
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.
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.
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.
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.