A counterexample guided abstraction refinement framework for verifying concurrent c programs
Sagar Chaki, Edmund M. Clarke · 2005
The ability to reason about the correctness of programs is no longer a subject of primarily academic interest. With each passing day the complexity of software artifacts being produced and employed is increasing dramatically. There is hardly any aspect of our day-to-day lives where software agents do not play an often silent yet crucial role. The fact that many of such roles are safety-critical mandates that these software artifacts be validated rigorously before deployment. So far, however, this goal has largely eluded us. In this article we will first layout the problem space which is of concern to my thesis, viz., automated formal verification of concurrent programs. We will present the core issues and problems, as well as the major paradigms and techniques that have emerged in our search for effective solutions. We will highlight the important hurdles that remain to be scaled. The later portion of this article presents an overview of the major techniques proposed in my thesis to surmount these hurdles. The article ends with a summary of the core contributions of my dissertation. Software Complexity