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 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. s: Program analysis, abstract interpretation, model checking, CTL.

• Type: Conference
• Year: 2001
• Where: CASCON
• Authors: Marsha Chechik, Wei Ding
• Keywords: CASCON 2001, CASCON 2007, Model Checking, Scalable Program Tool, Step-wise Automatic Verification