Components and program analyses
Matthias Felleisen · ACM SIGSOFT Software Engineering Notes · 2000
Model checking has been applied quite successfully to hardware verification and shows promise for software verification. The key obstacle is the well-known state explosion problem. This report describes work done by the investigator under NSF support, in particular grants CCR 980-4736 and CCR 941-5496, to ameliorate state explosion.