Grand Challenge: Model Check Software
Edmund M. Clarke, Himanshu Jain, Nishant Sinha · 2005
Abstract. Model checking has been successfully employed for verification of industrial hardware systems. Recently, model checking techniques have also enjoyed limited success in verifying software systems, viz., device drivers. However, there are several hurdles which must be overcome before model checking can be used to handle industrial-scale software systems. This article reviews some of the prominent model checking techniques being used for verification of software and summarizes the existing challenges in the field. Keywords. Software model checking. Counterexample-guided abstraction refinement. 1.