Decision Procedures for Large Scale Model Checking

项目ID: CCF-0541444 PI: Somenzi， Fabio Institution: University of Colorado at 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.