Lightweight Reasoning about Program Correctness

Automated verification tools vary widely in the types of properties they are able to analyze, the complexity of their algorithms, and the amount of necessary user involvement. In this paper we propose a framework for step-wise automatic verification and describe a lightweight scalable program analysis tool that combines abstraction and model checking. The tool guarantees that its True and False answers are sound with respect to the original system. We also check the effectiveness of the tool on an implementation of the Safety-Injection System.