Decision Procedures - Taschenbuch

Buch in der Datenbank seit 2019-01-12T18:09:37+01:00 (Berlin)
Detailseite zuletzt geändert am 2024-03-04T15:03:10+01:00 (Berlin)
ISBN/EAN: 9783662570654

ISBN - alternative Schreibweisen:
3-662-57065-3, 978-3-662-57065-4

Daten vom Verlag:

Autor/in: Daniel Kroening; Ofer Strichman
Titel: Texts in Theoretical Computer Science. An EATCS Series; Decision Procedures - An Algorithmic Point of View
Verlag: Springer; Springer Berlin
356 Seiten
Erscheinungsjahr: 2018-07-13
Berlin; Heidelberg; DE
Gedruckt / Hergestellt in Niederlande.
Sprache: Englisch
53,49 € (DE)
54,99 € (AT)
59,00 CHF (CH)
POD
XXI, 356 p. 64 illus., 5 illus. in color.

BC; Hardcover, Softcover / Informatik, EDV/Informatik; Theoretische Informatik; Verstehen; Informatik; Decision Procedures; Propositional Logic; Pointer Logic; Boolean Satisfiability Solver (SAT); Quantified Formulas; Satisfiability Modulo Theories (SMT); Constraint Satisfaction Problem (CSP); Theory of Computation; Software Engineering; Optimization; Software Engineering; Optimierung; BB

A decision procedure is an algorithm that, given a decision problem, terminates with a correct yes/no answer. Here, the authors focus on theories that are expressive enough to model real problems, but are still decidable. Specifically, the book concentrates on decision procedures for first-order theories that are commonly used in automated verification and reasoning, theorem-proving, compiler optimization and operations research. The techniques described in the book draw from fields such as graph theory and logic, and are routinely used in industry.

) framework. Then, in separate chapters, they study decision procedures for propositional logic; equalities and uninterpreted functions; linear arithmetic; bit vectors; arrays; pointer logic; and quantified formulas. They also study the problem of deciding combined theories based on the Nelson-Oppen procedure.

rner and Leonardo de Moura, and Hillel Kugler, respectively.

Each chapter includes a detailed bibliography and exercises. Lecturers’ slides and a C++ library for rapid prototyping of decision procedures are available from the authors’ website.

Introduction and Basic Concepts.- Decision Procedures for Propositional Logic.- From Propositional to Quantifier-Free Theories.- Equalities and Uninterpreted Functions.- Linear Arithmetic.- Bit Vectors.- Arrays.- Pointer Logic.- Quantified Formulas.- Deciding a Combination of Theories.- Propositional Encodings.- Applications in Software Engineering.- SMT-LIB 2.0: A Brief Tutorial.- A C++ Library for Developing Decision Procedures.

A decision procedure is an algorithm that, given a decision problem, terminates with a correct yes/no answer. Here, the authors focus on theories that are expressive enough to model real problems, but are still decidable. Specifically, the book concentrates on decision procedures for first-order theories that are commonly used in automated verification and reasoning, theorem-proving, compiler optimization and operations research. The techniques described in the book draw from fields such as graph theory and logic, and are routinely used in industry.

) framework. Then, in separate chapters, they study decision procedures for propositional logic; equalities and uninterpreted functions; linear arithmetic; bit vectors; arrays; pointer logic; and quantified formulas. They also study the problem of deciding combined theories based on the Nelson-Oppen procedure.

rner and Leonardo de Moura, and Hillel Kugler, respectively.

Each chapter includes a detailed bibliography and exercises. Lecturers’ slides and a C++ library forrapid prototyping of decision procedures are available from the authors’ website.