Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
type: Item
instance of: scholarly article
title: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
zbMATH Open document ID: 1149.68071
author: Daniel Kroening
author: Ofer Strichman
published in: Texts in Theoretical Computer Science. An EATCS Series
publication date: 2008-02-27T00:00:00Z
review text: This book has two topics as main points: ``decision procedures'' and ``algorithms to be applied for these decisions''. This is a very interesting approach because in real life (i.e. in the application area) a given problem is what comes first, and then solutions have to be found, and mostly there is a broad range of possibilities for the solutions. Since real problems tend to be very large and complex, the creation of appropriate solutions by means of algorithms and software is the final target. Such an approach is very useful for graduate students or students in year four or five, since their knowledge is already broad enough to study several topics covered by the book. As can be seen by the sequence of topics, the knowledge covered is very extensive and gives an impressive example what could or should be done in education to prepare for real-life problems. The theoretical background is based on first-order theories, but in many different ways. It starts with methods and technologies that are based on propositional logics, such as SAT solvers and binary decision diagrams, followed by equality logic and uninterpreted functions. The next chapters deal with linear arithmetic, bit vectors, arrays, pointer logic, quantified formulas, deciding combinations of theories and propositional encodings. Some hints to a C++ library for the development of decision procedures close the book. Each chapter introduces and explains a lot of different concepts and presents good examples, some problems and exercises with algorithm-based solutions, and a glossary at its end, which makes the book very applicable and readable. The book is very well written and interesting to read. As a textbook for students it will require hard work to fully understand it and go through it. It might also be useful to use it in parts.
reviewed by: Christian Posthoff
Mathematics Subject Classification ID: 68-01
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 68T27
zbMATH DE Number: 5241506
zbMATH Keywords: decision algorithms
zbMATH Keywords: propositional logic
zbMATH Keywords: first-order theory
describes a project that uses: Quaffle
MaRDI profile type: Publication
Recommended article: Decision procedures. An algorithmic point of view
Recommended article: Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view
Recommended article: Book review of: D. Kroening and O. Strichman, Decision procedures. An algorithmic point of view. 2nd ed.
Recommended article: Q4359172
Recommended article: Decision algorithms for some fragments of analysis and related areas
Recommended article: Q4484923
Recommended article: Axioms for a Class of Algorithms of Sequential Decision Making
Recommended article: Optimal decision processes and algorithms
Recommended article: On the Asymptotic Behavior of Decision Procedures
description: scientific article