>>>>> "B" == <Bertrand> writes:
B> hello,
B> I'm a belgian student presently working on model checking for my thesis.
B> I'm looking for more details on the power, weaknesses, and optimisations
B> made by using the particular 'invariant check' algorithm you use in you
B> VIS tool.
B> Could you give me some reference about this?
B> Thanks a lot, and good furtherwork.
B> Bertrand.
The check_invariant command of VIS works by forward reachability
analysis. As all algorithms in VIS 1.4, it uses BDDs for the
representation of the transition relation and the sets of states.
Among the features of the algorithm:
1. Cone-of-influence reduction.
2. Early termination.
3. Ability to use over- and under-approxiamtions of the reachable
states. How this is done is described in a number of papers,
including
@INPROCEEDINGS { Moon98 ,
ADDRESS = "San Jose, CA" ,
AUTHOR = "I.-H. Moon and J.-Y. Jang and G. D. Hachtel and F. Somenzi and C. Pixley and J. Yuan" ,
BOOKTITLE = iccad ,
MONTH = nov ,
PAGES = "351-358" ,
TITLE = "Approximate Reachability Don't Cares for {CTL} Model Checking" ,
YEAR = "1998"
}
@INPROCEEDINGS { Ravi99 ,
ADDRESS = "Berlin" ,
AUTHOR = "K. Ravi and F. Somenzi" ,
BOOKTITLE = "Correct Hardware Design and Verification Methods (CHARME'99)" ,
MONTH = sep ,
NOTE = "LNCS 1703" ,
PAGES = "250-264" ,
PUBLISHER = "Springer-Verlag" ,
TITLE = "Hints to Accelerate Symbolic Traversal" ,
YEAR = "1999"
}
@INPROCEEDINGS { Ravi99c ,
ADDRESS = "Austin, TX" ,
AUTHOR = "K. Ravi and F. Somenzi" ,
BOOKTITLE = iccd ,
MONTH = oct ,
PAGES = "467-474" ,
TITLE = "Efficient Fixpoint Computation for Invariant Checking" ,
YEAR = "1999"
}
@INPROCEEDINGS { Moon99b ,
ADDRESS = "San Jose, CA" ,
AUTHOR = "I.-H. Moon and J. Kukula and T. Shiple and F. Somenzi" ,
BOOKTITLE = iccad ,
MONTH = nov ,
PAGES = "41-44" ,
TITLE = "Least Fixpoint Approximations for Reachability Analysis" ,
YEAR = "1999"
}
Fabio
This archive was generated by hypermail 2b30 : Tue Mar 05 2002 - 12:29:22 MST