• A new combination of forwards and backwards abstract fixed-point model-checking computations for universal safety. It computes a more precise result than that computed by conjunction of the forward and backward analyses alone, without needing to refine the abstraction;
• When abstraction is unsound (as can happen in minimum/maximum path-length problems), it is proposed to use the partial results of a classical combination of forward and backward abstract interpretation analyses for universal safety in order to reduce, on-the-fly, the concrete state space to be searched by model-checking.

\bibitem{CousotCousot99-1}
P.~Cousot and R.~Cousot.
\newblock Refining model checking by abstract interpretation
\newblock \emph{Automated Software Engineering Journal}, 6(1):69--95, 1999.

@article{CousotCousot99-1,
   author =  {Cousot, P{.} and Cousot, R{.}},
   title =   {Refining Model Checking by Abstract Interpretation},
   journal = {Automated Software Engineering},
   volume =  6,
   number = 1,
   pages =   {69--95},
   year =    1999,
}