LIVE and SLICE are static analysis tools for IF specifications developed by Grenoble (UJF).
LIVE performs live variables optimization: it transforms an IF specification into an equivalent one by adding systematic resets of non-live variables. This transformation preserves completely the behavior of the original specification while the global state space (and further, the exploration time) are dramatically reduced.
SLICE performs reduction techniques inspired from program slicing. These techniques allow to extract from a model portions which are relevant to the validation of the properties under consideration. This extraction is done by projecting a model on a set of relevant actions ; it can be seen as an action-based abstraction technique. Slicing allows to obtain smaller IF models with manageable state graphs.