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.