SHF: Small: Pushing the Frontier of Linear-Time Model-Checking Technology

模型检测是一种用于验证计算机系统正确性的技术。不同的实现方式在当今广泛的工业使用中。然而，在我们对模型检测所涉及的算法问题的理解方面仍然存在许多巨大的差距，并且该技术仍然受到工业设计的极大挑战。例如，在硬件设计验证中，几乎不可能应用现有工具来完成具有明确功能的单元。该项目正在推动这一技术的前沿，其目标是通过开发新的可扩展的模型检查算法来扩展其对功能系统单元的适用性。其结果将是提高计算机系统的可靠性。这个项目将探讨设计验证的数学方法，使用自动机理论作为设计规范和验证的统一范例。自动机理论的方法分离的逻辑和组合方面的推理系统。规范到自动机的转换处理了逻辑，并将所有的组合困难转移到关于自动机的问题上，从而产生干净且渐近最优的算法。虽然基本理论已经很好地理解，但仍然存在许多具有挑战性的差距，改进的算法可以显着提高这种方法的可扩展性。这个项目研究了改进自动机理论算法的方法，使它们更适合大规模的模型检测。

Model checking is a technique for verifying the correctness of computer systems. Different implementations are in wide industrial usage today. There are still, however, many large gaps in our understanding of the algorithmic issues involved in model checking, and the technology is still greatly challenged by industrial designs. For example, in hardware-design verification, it is rarely possible to apply existing tools to complete units with clear functionality. This project is pushing the frontier of this technology with the goal of scaling its applicability to functional system units by developing novel scalable algorithms for model checking. The result will be increased reliability of computer systems. This project will explore the mathematical approach to design verification that uses automata theory as a unifying paradigm for design specification and verification. The automata-theoretic approach separates the logical and the combinatorial aspects of reasoning about systems. The translation of specifications to automata handles the logic and shifts all the combinatorial difficulties to questions about automata, yielding clean and asymptotically optimal algorithms. While the fundamental theory is well understood, there are still many challenging gaps and improved algorithms can enhance the scalability of this approach significantly. This project investigates ways of improving automata-theoretic algorithms so they are more suitable for model checking at scale.