Better verification through symmetry

This work provides a proof of the soundness of the new symmetry-based verification algorithm based on a definition of the formal semantics of a simple description language with scalarsets, and leads to an alternative characterization of data independence.

Abstract

A fundamental difficulty in automatic formal verification of finite-state systems is thestate explosion problem—even relatively simple systems can produce very large state spaces, causing great difficulties for methods that rely on explicit state enumeration. We address the problem by exploiting structuralsymmetries in the description of the system to be verified. We make symmetries easy to detect by introducing a new data typescalarset, a finite and unordered set, to our description language. The operations on scalarsets are restricted so that states are guaranteed to have the same future behaviors, up to permutation of the elements of the scalarsets. Using the symmetries implied by scalarsets, a verifier can automatically generate a reduced state space, on the fly. We provide a proof of the soundness of the new symmetry-based verification algorithm based on a definition of the formal semantics of a simple description language with scalarsets. The algorithm has been implemented and evaluated on several realistic high-level designs. Memory requirements were reduced by amounts ranging from 83% to over 99%, with speedups ranging from 65% to 98%. Symmetry-based reduction leads to an alternative characterization ofdata independence: a protocol is data-independent if there is a scalarset type not used as an array index orfor loop index. In this case, symmetry-based reduction converts an infinite state space to a finite state space. Unlike other methods that exploit data independence in verification, this reduction occurs completely automatically.