This report is a collection of six articles on model checking in the abstract/refinement framework. This framework is used by various techniques for tackling the state-space explosion problem that is frequently encountered in model checking.

The articles collected in this report include:

• Counterexample-Guided Abstraction Refinement
  Clarke, Grumberg, Jha, Lu, Veith
• SAT based Abstraction-Refinement using ILP and Machine Learning Techniques
  Clarke, Gupta, Kukula, Strichman
• Automated Abstraction Refinement for Model Checking
  Large State Spaces using SAT based Conflict Analysis
  Chauhan, Clarke, Kukula, Sapra, Veith, Wang
• SAT based Predicate Abstraction for Hardware Verification
  Clarke, Talupur, Wang
• High Level Verification of Control Intensive Systems Using Predicate Abstraction
  Clarke, Grumberg, Talupur, Wang
• Verification of Hybrid Systems Based on Counterexample-Guided
  Abstraction Refinement
  Clarke, Fehnker, Han, Krogh, Stursberg, Theobald

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu