没有合适的资源?快使用搜索试试~ 我知道了~
Decision Procedures
5星 · 超过95%的资源 需积分: 10 27 下载量 149 浏览量
2015-01-16
18:09:42
上传
评论
收藏 5.83MB PDF 举报
温馨提示
试读
314页
Decision Procedures - An Algorithmic Point of View
资源推荐
资源详情
资源评论
Texts in Theoretical Computer Science
An EATCS Series
Editors: W. Brauer J. Hromkovi
ˇ
c G. Rozenberg A. Salomaa
On behalf of the European Association
for Theoretical Computer Science (EATCS)
Advisory Board:
G. Ausiello M. Broy C.S. Calude A. Condon
D. Harel J. Hartmanis T. Henzinger T. Leighton
M. Nivat C. Papadimitriou D. Scott
Daniel Kroening · Ofer Strichman
Decision Procedures
An Algorithmic Point of View
Foreword by Randal E. Bryant
123
Daniel Kroening
Computing Laboratory
University of Oxford
Wolfson Building
Parks Road
Oxford, OX1 3QD
United Kingdom
daniel.kroening@comlab.ox.ac.uk
Ofer Strichman
William Davidson Faculty of Industrial
Engineering and Management
Technion – Israel Institute of Technology
Technion City
Haifa 32000
Israel
ofers@ie.technion.ac.il
ISBN 978-3-540-74104-6 e-ISBN 978-3-540-74105-3
Texts in Theoretical Computer Science. An EATCS Series. ISSN 1862-4499
Library of Congress Control Number: 2008924795
ACM Computing Classification (1998): B.5.2, D.2.4, D.2.5, E.1, F.3.1, F.4.1
c
2008 Springer-Verlag Berlin Heidelberg
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is
concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting,
reproduction on microfilm or in any other way, and storage in data banks. Duplication of this publication
or parts thereof is permitted only under the provisions of the German Copyright Law of September 9,
1965, in its current version, and permission for use must always be obtained from Springer. Violations
are liable to prosecution under the German Copyright Law.
The use of general descriptive names, registered names, trademarks, etc. in this publication does not
imply, even in the absence of a specific statement, that such names are exempt from the relevant protective
laws and regulations and therefore free for general use.
Cover Design: K
¨
unkelLopka GmbH, Heidelberg
Printed on acid-free paper
987654321
springer.com
Foreword
By Randal E. Bryant
Research in decision procedures started several decades ago, but both their
practical importance and the underlying technology have progressed rapidly
in the last five years. Back in the 1970s, there was a flurry of activity in this
area, mostly centered at Stanford and the Stanford Research Institute (SRI),
motivated by a desire to apply formal logic to problems in artificial intelligence
and software verification. This work laid foundations that are still in use today.
Activity dropped off through the 1980s and 90s, accompanied by a general
pessimism about automated formal methods. A conventional wisdom arose
that computer systems, especially software, were far too complex to reason
about formally.
One notable exception to this conventional wisdom was the success of
applying Boolean methods to hardware verification, beginning in the early
1990s. Tools such as model checkers demonstrated that useful properties could
be proven about industrial scale hardware systems, and that bugs could be
detected that had otherwise escaped extensive simulation. These approaches
improved on their predecessors by employing more efficient logical reasoning
methods, namely ordered binary decision diagrams and Boolean satisfiability
solvers. The importance of considering algorithmic efficiency, and even low-
level concerns such as cache performance became widely recognized as having
a major impact on the size of problems that could be handled.
Representing systems at a detailed Boolean level limited the applicability
of early model checkers to control-intensive hardware systems. Trying to model
data operations, as well as the data and control structures found in software
leads to far too many states, when every bit of a state is viewed as a separate
Boolean signal.
One way to raise the level of abstraction for verifying a system is to view
data in more abstract terms. Rather than viewing a computer word as a
collection of 32 Boolean values, it can be represented as an integer. Rather
than viewing a floating point multiplier as a complex collection of Boolean
functions, many verification tasks can simply view it as an “uninterpreted
剩余313页未读,继续阅读
资源评论
- Kelvinordic2020-12-22The authors introduce the basic terminology of SAT, Satisfiability Modulo Theories (SMT) and the DPLL(T) framework.
jiangdmdr
- 粉丝: 57
- 资源: 774
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功