Automatic Property Checking for Software: Past, Present and Future

Summary form only given. Over the past few years, we have seen several automatic static analysis tools being developed and deployed in industrial-strength software development. I will survey several of these tools ranging from heuristic and scalable analysis tools (such as PREFix, PREFast and Metal), to sound analysis tools based on counter example driven refinement (such as SLAM). Then, I will present two exciting recent developments in counterexample driven refinement: (1) generalizing counterexample driven refinement to work with any abstract interpretation, and (2) combining directed testing with counterexample driven refinement