Lightweight Reasoning about Program Correctness
Marsha Chechik () and
Wei Ding ()
Additional contact information
Marsha Chechik: University of Toronto
Wei Ding: University of Toronto
Information Systems Frontiers, 2002, vol. 4, issue 4, No 2, 363-377
Abstract:
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-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.
Keywords: program analysis; abstract interpretation; model checking; CTL (search for similar items in EconPapers)
Date: 2002
References: View complete reference list from CitEc
Citations:
Downloads: (external link)
http://link.springer.com/10.1023/A:1020883625495 Abstract (text/html)
Access to the full text of the articles in this series is restricted.
Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.
Export reference: BibTeX
RIS (EndNote, ProCite, RefMan)
HTML/Text
Persistent link: https://EconPapers.repec.org/RePEc:spr:infosf:v:4:y:2002:i:4:d:10.1023_a:1020883625495
Ordering information: This journal article can be ordered from
http://www.springer.com/journal/10796
DOI: 10.1023/A:1020883625495
Access Statistics for this article
Information Systems Frontiers is currently edited by Ram Ramesh and Raghav Rao
More articles in Information Systems Frontiers from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().