Model Checking and Beyond

长期以来，人们一直需要更有效的方法来设计正确和健壮的计算机软件以及硬件。 一种称为“模型检查”的方法已经开发出来，提供了一种算法手段，用于建立名义上有限状态程序的正确性。IBM、Intel和Motorola等计算机制造商发现模型检验对于验证中等规模的计算机硬件电路很有用。 然而，模型检测可以成功地应用于大型硬件设计和软件之前，需要进一步的研究。 软件比硬件更难构建和验证，因为它的组织不太统一，规模很大。 本课程将研究基于偏序和非对称性简化的非规则组织技术，以促进模型检测在大型软件系统中的应用。其他主要研究课题包括：新的和改进的基本技术，包括抽象、算法和数据结构，以提高模型检测的效率;模型检测与其他程序设计方法的集成;通过模型检测的自动程序综合;以及使用更丰富的程序鲁棒性概念来扩展传统模型检查的二分（正确/不正确）框架的可行性。

There is a chronic need for more effective methods of designing correct and robust computer software as well as hardware. A method called "Model Checking" has been developed, providing an algorithmic means for establishing correctness of nominally finite state programs. Computer manufacturerssuch as IBM, Intel, and Motorola are finding model checking useful for verifying computer hardware circuits of moderate size. However, further research is required before model checking can be applied successfully to large hardware designs and to software. Software is more difficult to construct and verify than hardware due to its less uniform organization and sheer scale. Techniques to cope with irregular organization based on partial order and asymmetry reduction facilitating application of model checking to large software systems will be investigated.Other central topics of investigation include: new and improved basic techniques, including abstractions, algorithms, and data structures, for more efficient model checking; integration of model checking with other program design methods; automatic program synthesis via model checking; and the feasibility of extending the dichotomous (correct/incorrect) framework of conventional model checking using richer program robustness notions.