Lightweight Reasoning about Program Correctness

被引：0
作者：
Marsha Chechik
Wei Ding
机构：
[1] University of Toronto,Department of Computer Science
来源：
Information Systems Frontiers | 2002年 / 4卷
关键词：
program analysis; abstract interpretation; model checking; CTL;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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.
引用
收藏
页码：363 / 377
页数：14
相关论文
共 38 条
[1]  
Bruns G(1999)Model checking partial state spaces with 3-valued temporal logics Proceedings of CAV’99 1633 274-287
[2]  
Godefroid P.(2000)Generalized model checking: Reasoning about partial state spaces Proceedings of CONCUR’00 877 168-182
[3]  
Bruns G(2000)Composite model checking: Verification with type-specific symbolic representations ACM Transactions on Software Engineering and Methodology 9 3-50
[4]  
Godefroid P.(2001)Model-checking over multi-valued logics Proceedings of Formal Methods Europe (FME’01) 2021 72-98
[5]  
Bultan T(1986)Automatic verification of finitestate concurrent systems using temporal logic specifications ACM Transactions on Programming Languages and Systems 8 244-263
[6]  
Gerber R(1995)Verification of the futurebus+ cache coherence protocol Formal Methods in System Design 6 217-232
[7]  
League C.(1999)Refining model checking by abstract interpretation Authomated Software Engineering, special issue on Automated Software Analysis 6 69-95
[8]  
Chechik M(1997)Abstract interpretation of reactive systems ACMTransactions on Programming Languages and Systems 2 253-291
[9]  
Easterbrook S(1997)The model checker SPIN IEEE Transactions on Software Engineering 23 279-295
[10]  
Petrovykh V.(2001)Modal transition systems: A foundation for three-valued program analysis Proceedings of 10th European Symposium on Programming (ESOP) 2028 155-169
1234