Lightweight Reasoning About Program Correctness
Abstract
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-wize 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.