Combining Theorem Proving with Model Checking through Predicate Abstraction.

The article discusses the hybrid computer system verification process that combines theorem proving with model checking through predicate abstraction. The author contends that there is a gap in the complexity verification tools can handle and practical verification problems that can be lessened via theorem proving with model checking through predicate abstraction.