NSF-CNPq Collaborative Research: Formal Verification of Computer Systems in Industrial Complexity

9900309 Edmund clark模型检查是有限状态并发系统（如顺序电路设计和通信协议）的自动验证技术。通过使用像二元决策图这样的特殊数据结构，可以验证具有大量可达状态的极其复杂系统的属性。虽然这项技术已经被主要的高科技公司使用，但还需要进一步的研究才能充分发挥这种方法的潜力。当前工具所能处理的问题的规模是有限的。这项研究的目标之一是追求一些项目，这些项目将解决状态爆炸问题，并允许验证更大的系统，其中一些比目前可能的大很多个数量级。另一个目标是将模型检查技术扩展到目前不能直接处理的不同类型的系统。传统上，模型检查应用于硬件设计，后来扩展到其他类型的系统，如实时系统。我们相信，将模型检验应用于不同类型的系统，如随机系统，可以开辟新的研究领域，并有助于解决实际应用中的重要问题。这项工作将与米纳斯吉拉斯州联邦大学的Sergio Campos和北巴西格兰德州联邦大学的David Deharbe合作完成，后者将得到巴西国家石油公司的支持。

9900309 Edmund ClarkModel checking is an automatic verification technique for finite state concurrent systems such as sequential circuit designs and communication protocols. By using special data structures like binary decision diagrams, it is possible to verify properties of extremely complex systems with immense numbers of reachable states. Although the technique is already in use by major high-tech firms, additional research is needed to realize the full potential of the method. There is a limit on the size of problems that can be handled by current tools. One of the goals of this research is to pursue a number of projects that will attack the state explosion problem and allow larger systems to be verified, some many orders of magnitude larger than currently possible. Another goal is to extend model checking techniques to different types of systems that cannot be directly handled today. Traditionally, model checking has been applied to hardware designs, being later extended to other types of systems such as real-time systems. We believe that applying model checking to different types of systems such as stochastic systems can open up new areas of research and help solve important problems with practical applications. The work will be done in collaboration with Sergio Campos of the Federal University of Minas Gerais and David Deharbe of the Federal University of Rio Grande do Norte, who will be supported by CNPq of Brazil.