首页    期刊浏览 2025年06月20日 星期五
登录注册

文章基本信息

  • 标题:Predicate Abstraction via Symbolic Decision Procedures
  • 本地全文:下载
  • 作者:Shuvendu Kumar Lahiri ; Thomas Ball ; Byron Cook
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2007
  • 卷号:3
  • 期号:02
  • DOI:10.2168/LMCS-3(2:1)2007
  • 出版社:Technical University of Braunschweig
  • 摘要:

    We present a new approach for performing predicate abstraction based on symbolic decision procedures. Intuitively, a symbolic decision procedure for a theory takes a set of predicates in the theory and symbolically executes a decision procedure on all the subsets over the set of predicates. The result of the symbolic decision procedure is a shared expression (represented by a directed acyclic graph) that implicitly represents the answer to a predicate abstraction query. We present symbolic decision procedures for the logic of Equality and Uninterpreted Functions (EUF) and Difference logic (DIFF) and show that these procedures run in pseudo-polynomial (rather than exponential) time. We then provide a method to construct symbolic decision procedures for simple mixed theories (including the two theories mentioned above) using an extension of the Nelson-Oppen combination method. We present preliminary evaluation of our Procedure on predicate abstraction benchmarks from device driver verification in SLAM.

  • 关键词:Decision Procedures;Uninterpreted Functions;Device Drivers
国家哲学社会科学文献中心版权所有