Decision Procedures for Large Scale Model Checking

大规模模型检查的决策程序

• 批准号: 0541444
• 负责人: Fabio Somenzi
• 金额: $ 30万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-10-01 至 2009-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541444&HistoricalAwards=false
• 关键词: Decision; Procedures; Large; Scale; Model

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.

Prop ID：ccf-0541444 PI：Somezi，Fabio Institution：科罗拉多大学博尔德分校标题：Decision Procedure for Large Scale Model Checking简介在系统设计中更广泛地使用形式化方法(如模型检查)现有的主要障碍是算法的有限容量。虽然形式验证中的大多数关键问题在理论上都是难以解决的，但过去十年见证了算法的改进，极大地扩展了可以严格和自动完成的领域。能力的持续增长是大多数大型电子设计组织的优先事项。最近形式验证技术在抽象细化和基于命题可满足性的程序方面的进展尤为显著。通过巧妙地使用决策程序，甚至通过不同方法的合作，这些进展成为可能。然而，在通过更深层次的整合来利用不同方法的优势方面，几乎没有做什么。当前的技术通常在需要结合不同方法的优点的问题上失败，而不是从工具箱中选择合适的方法。这项提议的目的是追求这种整合，并探索从认识到基于抽象的模型检查和决策程序的分离是一种人为的分离所带来的好处。预期的结果是一种有效的大规模模型检验策略，代表着能力的显著飞跃。可满足性(SAT)求解器的长处和弱点是他们的遗忘能力。虽然定点计算累积的状态集的表示通常变得笨拙，但SAT求解器原则上可以避免保存除决策堆栈以外的任何有关搜索的信息。遗忘的代价是重复，即使现代的SAT程序记录了冲突条款，人们也会遇到这样的问题，因为它们无法代表已经解决的子问题的相关信息。拟议的研究将在基于抽象的模型检测的背景下解决这一问题。对于可满足性的其他应用和组合搜索的一般问题，也有望产生显著的影响。