With the steady increase in computational power of general purpose computers, our ability to analyze routine software artifacts is also steadily increasing. As a result, we are witnessing a shift in emphasis from the verificaabstract hand-built models of code, towards the direct verification of implementation level code. This change in emphasis poses a new set of challenges in software verification. We explore some of them in this paper.
Gerard J. Holzmann