Model checking has won some industrial acceptance in debugging designs. Theorem proving and formal verification are less popular. An approach built around automated abstractions could integrate theorem proving with model checking in an acceptable way and provide a bridge between refutation and verification.

• forte-pstv2000-slides.ps
• forte-pstv2000.ps