Counterexample-Guided Abstraction Refinement

xample-Guided Abstraction Refinement for Symbolic Model Checking EDMUND CLARKE YUAN LU Carnegie Mellon University, Pittsburgh, Pennsylvania Broadcom Co., San Jose, California ORNA GRUMBERG AND The Technion, Haifa, Israel HELMUT VEITH SOMESH JHA Vienna University of Technology, Wien, Austria University of Wisconsin, Madison, Wisconsin The state explosion problem remains a major hurdle in applying symbolic model checking hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight. A preliminary version of this article has been presented at the 2000 Conference on Computer-Aided Verification (CLARKE, E., GRUMBERG, O., JHA, S., LU, Y., AND VEITH, H. 2000. Counterexamplebstraction refinement. In Proceedings of the 2000 Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, New York. (Full version available a...

• Type: Conference
• Year: 2000
• Where: CAV
• Authors: Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
• Keywords: Carnegie Mellon University, CAV 2000, Computer-Aided Verification, Hardware, State Explosion Problem