Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27)
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.
- Decision procedures. An algorithmic point of view
- Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view
- Book review of: D. Kroening and O. Strichman, Decision procedures. An algorithmic point of view. 2nd ed.
- scientific article; zbMATH DE number 1071873
- Decision algorithms for some fragments of analysis and related areas
- scientific article; zbMATH DE number 1455133
- Axioms for a Class of Algorithms of Sequential Decision Making
- Optimal decision processes and algorithms
- On the Asymptotic Behavior of Decision Procedures
- Targeted and contextual redescription set exploration
- Propagation based local search for bit-precise reasoning
- On logical bifurcation diagrams
- Experience of improving the BLAST static verification tool
- Some results on parametric temporal logic
- Superposition as a decision procedure for timed automata
- Sharpening constraint programming approaches for bit-vector theory
- IPL: an integration property language for multi-model cyber-physical systems
- On neural network equivalence checking using SMT solvers
- Data abstraction: a general framework to handle program verification of data structures
- Region analysis for deductive verification of C programs
- Wombit: a portfolio bit-vector solver using word-level propagation
- A layered algorithm for quantifier elimination from linear modular constraints
- Metalevel algorithms for variant satisfiability
- Preface to the special issue ``SI: satisfiability modulo theories
- Abstract interpretation of microcontroller code: intervals meet congruences
- Satisfiability in composition-nominative logics
- SLAP: specification logic of actions with probability
- Range and set abstraction using SAT
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Colors Make Theories Hard
- Metalevel algorithms for variant satisfiability
- A survey of satisfiability modulo theory
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Semantically-guided goal-sensitive reasoning: model representation
- Decision procedures for region logic
- Matching multiplications in bit-vector formulas
- Mutation-Based Test Case Generation for Simulink Models
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- Virtual substitution for SMT-solving
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Propositional SAT solving
- SAT-Based Model Checking
- Satisfiability modulo theories
- Mining backbone literals in incremental SAT. A new kind of incremental data
- Integrating simplex with tableaux
- scientific article; zbMATH DE number 4053563 (Why is no real title available?)
- A pearl on SAT and SMT solving in Prolog
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Satisfiability checking: theory and applications
- An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic
- Runtime verification of embedded real-time systems
- scientific article; zbMATH DE number 7378548 (Why is no real title available?)
- Partial order reduction for deep bug finding in synchronous hardware
- Complexity of fixed-size bit-vector logics
- Loop invariants: analysis, classification, and examples
- Decision procedures. An algorithmic point of view
- Volume Computation for Boolean Combination of Linear Arithmetic Constraints
- Fixed points, Nash equilibria, and the existential theory of the reals
- Symbolic trajectory evaluation for word-level verification: theory and implementation
- Computer Aided Verification
- Transfer function synthesis without quantifier elimination
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- An Impossible Asylum
- Regular model checking revisited
- Experiments with automated reasoning in the class
- Synthesising programs with non-trivial constants
- Equality detection for linear arithmetic constraints
- Decision procedures for sequence theories
- Reasoning on data words over numeric domains
- The CDSAT method for satisfiability modulo theories and assignment: an exposition
- SMT-based and fixed-point approaches for state estimation in max-plus linear systems
- The QSMA algorithm for quantifiers in SMT
- Time-budgeting: a component based development methodology for real-time embedded systems
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
This page was built for publication: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2473386)
