Decision Procedures for Large Scale Model Checking

道具ID：CCF-0541444 PI：Somenzi，Fabio机构：位于Boulder的科罗拉多大学标题：大规模模型检查的决策程序 在系统设计中，模型检测等形式化方法的广泛应用面临的主要障碍是算法的能力有限。 虽然形式验证中的大多数关键问题在理论上是棘手的，但过去十年来，算法的改进大大扩展了严格和自动完成的范围。 不断提高验证能力是大多数大型电子设计机构的优先考虑事项。形式验证技术的最新进展在抽象细化和基于命题可满足性的过程中尤为显著。 这些进步是通过巧妙地使用决策程序甚至通过不同方法的合作而实现的。 然而，在通过更深层次的整合利用不同方法的优势方面几乎没有做什么。 目前的技术往往失败的问题，需要从不同的方法的优势相结合，而不是从工具箱中选择一个合适的方法。 这个建议的目的是追求这样的集成和探索的好处，来自实现基于抽象的模型检查和决策过程的分离是一个人为的。 预期的结果是大规模模型检测的有效策略，代表了容量的显著飞跃。可满足性（SAT）求解器的优点和缺点是它们的遗忘能力。 虽然不动点计算累积状态集，但其表示通常变得笨拙，SAT求解器原则上可以避免保存除决策堆栈之外的任何有关搜索的信息。 遗忘的代价是重复，即使现代SAT程序记录了冲突条款，人们也会遇到这样的问题，即这些程序由于无法表示已经解决的子问题的相关信息而陷入困境。 拟议的研究将解决这个问题的背景下，基于抽象的模型检查。 一个显着的影响，其他应用程序的可满足性和一般问题的组合搜索也预计。

Prop ID: CCF-0541444 PI: Somenzi, Fabio Institution: University of Colorado at Boulder Title: Decision Procedures for Large Scale Model Checking ABSTRACTThe major extant hurdle to a more widespread use of formal methods like model checking in systems design is the limited capacity of the algorithms. While most key problems in formal verification are theoretically intractable, the last decade has witnessed algorithmic improvements that have greatly extended the realm of what can be done both rigorously and automatically. Continued increase in capabilities is a priority for most large electronic design organizations.Recent advances in formal verification technology have been particularly remarkable in abstraction refinement and in the procedures based on propositional satisfiability. These advances have been made possible by clever uses of decision procedures and even by the cooperation of different approaches. However, little has been done in leveraging the strengths of different approaches via a deeper integration. Current techniques often fail on problems that require a combination of strengths from different approaches, rather than the choice of a suitable approach from a toolbox. The aim of this proposal is to pursue such integration and to explore the benefits that come from realizing that the separation of abstraction-based model checking and decision procedures is an artificial one. The anticipated result is an effective strategy for large scale model checking that represents a significant leap in capacity.The strength and, at the same time, weakness of satisfiability (SAT) solvers is their ability to forget. While fixpoint computations accumulate sets of states whose representations often become unwieldy, a SAT solver can, in principle, avoid saving any information about the search except for the decision stack. The price of forgetfulness is repetition, and even though modern SAT procedures record conflict clauses, one encounters problems where such procedures flounder because of their inability to represent the relevant information about subproblems already solved. The proposed research will address this issue in the context of abstraction-based model checking. A significant fallout for other applications of satisfiability and for the general problem of combinatorial search is also expected.