The Resource Decision procedures : an algorithmic point of view, Daniel Kroening, Ofer Strichman ; foreword by Randal E. Bryant

Decision procedures : an algorithmic point of view, Daniel Kroening, Ofer Strichman ; foreword by Randal E. Bryant

Label
Decision procedures : an algorithmic point of view
Title
Decision procedures
Title remainder
an algorithmic point of view
Statement of responsibility
Daniel Kroening, Ofer Strichman ; foreword by Randal E. Bryant
Creator
Contributor
Subject
Language
eng
Member of
Cataloging source
YDXCP
http://library.link/vocab/creatorName
Kroening, Daniel
Illustrations
illustrations
Index
index present
LC call number
QA279.4
LC item number
.K76 2008
Literary form
non fiction
Nature of contents
bibliography
http://library.link/vocab/relatedWorkOrContributorName
Strichman, Ofer
http://library.link/vocab/subjectName
  • Decision making
  • Algorithms
  • Logic, Symbolic and mathematical
  • Algorithms
  • Decision making
  • Logic, Symbolic and mathematical
  • Entscheidungsverfahren
  • Mathematische Logik
  • Theoretische Informatik
Summary expansion
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. The authors introduce the basic terminology of satisfiability modulo theories and then, in separate chapters, study decision procedures for each of the following theories: 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 and dedicate a chapter to modern techniques based on an interplay between a SAT solver and a decision procedure for the investigated theory. This textbook has been used to teach undergraduate and graduate courses at ETH Zurich, at the Technion, Haifa, and at the University of Oxford. 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
Label
Decision procedures : an algorithmic point of view, Daniel Kroening, Ofer Strichman ; foreword by Randal E. Bryant
Instantiates
Publication
Bibliography note
Includes bibliographical references (p. [285]-297) and index
Carrier category
volume
Carrier category code
nc
Carrier MARC source
rdacarrier
Content category
text
Content type code
txt
Content type MARC source
rdacontent
Contents
Introduction and basic concepts -- Decision procedures for propositional logic -- Equality logic and uninterpreted functions -- Decision procedures for equality logic and uninterpreted functions -- Linear arithmetic -- Bit vectors -- Arrays -- Pointer logic -- Quantified formulas -- Deciding a combination of theories -- Propositional encodings
Dimensions
24 cm.
Extent
xvi, 304 pages
Isbn
9783540741046
Lccn
2008924795
Media category
unmediated
Media MARC source
rdamedia
Media type code
n
Other physical details
illustrations
System control number
  • (OCoLC)209334215
  • (OCoLC)ocn209334215
Label
Decision procedures : an algorithmic point of view, Daniel Kroening, Ofer Strichman ; foreword by Randal E. Bryant
Publication
Bibliography note
Includes bibliographical references (p. [285]-297) and index
Carrier category
volume
Carrier category code
nc
Carrier MARC source
rdacarrier
Content category
text
Content type code
txt
Content type MARC source
rdacontent
Contents
Introduction and basic concepts -- Decision procedures for propositional logic -- Equality logic and uninterpreted functions -- Decision procedures for equality logic and uninterpreted functions -- Linear arithmetic -- Bit vectors -- Arrays -- Pointer logic -- Quantified formulas -- Deciding a combination of theories -- Propositional encodings
Dimensions
24 cm.
Extent
xvi, 304 pages
Isbn
9783540741046
Lccn
2008924795
Media category
unmediated
Media MARC source
rdamedia
Media type code
n
Other physical details
illustrations
System control number
  • (OCoLC)209334215
  • (OCoLC)ocn209334215

Library Locations

  • African Studies LibraryBorrow it
    771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Alumni Medical LibraryBorrow it
    72 East Concord Street, Boston, MA, 02118, US
    42.336388 -71.072393
  • Astronomy LibraryBorrow it
    725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US
    42.350259 -71.105717
  • Fineman and Pappas Law LibrariesBorrow it
    765 Commonwealth Avenue, Boston, MA, 02215, US
    42.350979 -71.107023
  • Frederick S. Pardee Management LibraryBorrow it
    595 Commonwealth Avenue, Boston, MA, 02215, US
    42.349626 -71.099547
  • Howard Gotlieb Archival Research CenterBorrow it
    771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Mugar Memorial LibraryBorrow it
    771 Commonwealth Avenue, Boston, MA, 02215, US
    42.350723 -71.108227
  • Music LibraryBorrow it
    771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Pikering Educational Resources LibraryBorrow it
    2 Silber Way, Boston, MA, 02215, US
    42.349804 -71.101425
  • School of Theology LibraryBorrow it
    745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350494 -71.107235
  • Science & Engineering LibraryBorrow it
    38 Cummington Mall, Boston, MA, 02215, US
    42.348472 -71.102257
  • Stone Science LibraryBorrow it
    675 Commonwealth Avenue, Boston, MA, 02445, US
    42.350103 -71.103784
Processing Feedback ...