CMU-CS-03-180
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-03-180

Advances in Counterexample-Guides
Abstraction/Refinement

Edmund M. Clarke, Ofer Strichman, Editors

September 2003

CMU-CS-03-180.ps
CMU-CS-03-180.pdf


Keywords: Model-checking, abstraction-refinement


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
91 pages


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

This page maintained by reports@cs.cmu.edu