Gopalakrishnan G. Computation Engineering: Applied Automata Theory and Logic

Springer, 2010. — 493 p.It takes more effort to verify that digital system designs are correct than it does to design them, and as systems get more complex the proportion of cost spent on verification is increasing (one estimate is that verification complexity rises as the square of design complexity).
Although this verification crisis was predicted decades ago, it is only recently that powerful methods based on mathematical logic and automata theory have come to the designers’ rescue. The first such method was equivalence checking, which automates Boolean algebra calculations. Next came model checking, which can automatically verify that designs have – or don’t have – behaviours of interest specified in temporal logic. Both these methods are available today in tools sold by all the major design automation vendors.
It is an amazing fact that ideas like Boolean algebra and modal logic, originating from mathematicians and philosophers before modern computers were invented, have come to underlie computer aided tools for creating hardware designs.
The recent success of ’formal’ approaches to hardware verification has lead to the creation of a new methodology: assertion based design, in which formal properties are incorporated into designs and are then validated by a combination of dynamic simulation and static model checking. Two industrial strength property languages based on temporal logic are undergoing IEEE standardisation.
It is not only hardware design and verification that is changing: new mathematical approaches to software verification are starting to be deployed. Microsoft provides windows driver developers with verification tools based on symbolic methods.
Discrete mathematics, logic, automata, and the theory of computability are the basis for these new formal approaches. Although they have long been standard topics in computer science, the uses made of them in modern verification are quite different to their traditional roles, and need different mathematical techniques. The way they are taught often puts more emphasis on cultivating ‘paper and pencil’ proof skills, and less on their practical applications and implementation in tools. Topics in logic are often omitted, or taught without emphasizing connections with automata, and without explaining the algorithms (e.g., fixed-point computation) used in verification.
This classroom-tested undergraduate textbook is unique in presenting logic and automata theory as a single subject. Public domain software is used to animate the theory, and to provide a hands-on taste of the algorithms underlying commercial tools. It is clearly written and charmingly illustrated. The author is a distinguished contributor to both theory and to new tool implementation methods.
I highly recommend this book to you as the best route I know into the concepts underlying modern industrial formal verification.Mathematical Preliminaries
Cardinalities and Diagonalization
Binary Relations
Mathematical Logic, Induction, Proofs
Dealing with Recursion
Strings and Languages
Machines, Languages, DFA
NFA and Regular Expressions
Operations on Regular Machinery
The Automaton/Logic Connection, Symbolic Techniques
The ‘Pumping’ Lemma
Context-free Languages
Push-down Automata and Context-free Grammars
Turing Machines
Basic Undecidability Proofs
Advanced Undecidability Proofs
Basic Notions in Logic including SAT
Complexity Theory and NP-Completeness
DFA for Presburger Arithmetic
Model Checking: Basics
Model Checking: Temporal Logics
Model Checking: Algorithms
Conclusions
Book web site and tool information
BED Solution to the tic-tac-toe problem