Abstract

This paper grew out of our experiences with software model checking after several years of using static analysis to find errors.