C. Norris Ip, "Generalized Reversible Rules",
International Conference on Formal Methods in Computer-Aided
Design, November 1998.
Abstract: A generalized notion of
reversible rules is presented in this paper to perform state reduction
in automatic formal verification. The key idea is that some of the
transition rules in a design may be invertible, and therefore, they
can be used to collapse subgraphs into abstract states, thereby
reducing the state explosion problem. This paper improves upon
previous work to achieve the following goals: 1) the definition of
reversible rules is simpliified so that it is easy to apply the
reduction method on practice; 2) the definition is generalized to
allow more reduction in the size of the state graph.
The
reduction algorithm can be combined with symmetry reduction
techniques, for verification of invariants, deadlock-freedom, and
stuttering-invariant temporal properties.
C. Norris Ip and David L. Dill,
"Verifying Systems with Replicated Components in Murphi",
International Conference on Computer-Aided Verification,
pp. 147-158, July-August 1996.
postscript version
Abstract: We present an extension to the Murphi verifier to verify
systems with replicated identical components . Verification is by
explicit state enumeration in an abstract state space where states do
not record the exact numbers of components.
Through a new datatype, called RepetitiveID , the user
can suggest the use of such an abstraction to verify a
system of fixed size. Murphi automatically checks the soundness of the
abstract state graph, and automatically constructs the abstract state
graph using the system description.
Using a simple run time check, Murphi can also determine if it can
generalize the verification result of a system with fixed size to
systems of larger sizes, including the system with infinite number of
components.
C. Norris Ip and David L. Dill,
"State Reduction Using Reversible Rules",
33nd Design Automation Conference, pp. 564-567,
June, 1996.
postscript version
Abstract: We reduce the state explosion problem in automatic
verification of finite state systems by automatically collapsing
subgraphs of the state graph into abstract states. The key idea of
the method is to identify state generateion rules that can be
invertted. It can be used for verifcation of deadlock-freedom, error
and invariant checking and stuttering-inveariant CTL model checking.
C. Norris Ip and David L. Dill,
"Efficient Verification of Symmetric Concurrent Systems",
IEEE International Conference on Computer Design:
VLSI in Computers and Processors,
Cambridge, MA, October 3-6, 1993.
postscript version
Summary:
Previously, we proposed a reduction technique based
on symmetries to alleviate the state explosion problem in automatic
verification of concurrent systems. This paper describes the results
of testing the technique on a wide range of algorithms and protocols,
including realistic multiprocessor synchronization algorithms and
cache coherence protocols.
Memory requirements were reduced by amounts ranging from 83% to over
99%, and time requirements were often reduced as well. We also
consider the effectiveness of the technique on different types of
symmetries, such as symmetries in identical system components and
symmetries in data values.)
C. Norris Ip and David L. Dill,
"Better Verification Through Symmetry",
Proc. 11th International Symposium on
Computer Hardware Description Languages and Their Application,
April 1993.
postscript version
Summary:
We address the state explosion problem in automatic verification
of finite-state systems by exploiting symmetries in the
system description.
We also make symmetries easy to detect by introducing a new data type
scalarset, a finite and unordered set, to our description language.
In some cases, this method can collapse infinite state spaces into
finite spaces. We call this property data saturation.
Data saturation can be used to exploit data-independence
of protocols automatically, without hand-modification of the
protocol descriptions.