Abstract: Model checking and refinement checking are two major paradigms in automated verification. Of late there has been considerable resurgence of interest in automatically verifying software written in languages like C and Java. Most of these efforts (e.g. Bandera, SLAM, JPF) are based on model checking or more precisely trace containment. In this talk I will present ongoing work that investigates the prospects and challenges of software verification using refinement checking. I will discuss how we are planning to handle C programs and to use predicate abstraction and static analysis techniques in achieving our goal. I will conclude with out roadmap which includes extending our system for Java and incorporating notions of abstraction refinement and proof-carrying-code.