Automatic generation of invariants and intermediate assertions

被引:68
作者
Bjorner, N
Browne, A
Manna, Z
机构
[1] Computer Science Department, Stanford University, Stanford
基金
美国国家科学基金会; 美国国家航空航天局;
关键词
D O I
10.1016/S0304-3975(96)00191-0
中图分类号
TP301 [理论、方法];
学科分类号
081202 [计算机软件与理论];
摘要
Verifying temporal specifications of reactive and concurrent systems commonly relies on generating auxiliary assertions and on strengthening given properties of the system. This can be achieved by two dual approaches: The bottom-up method performs an abstract forward propagation (computation) of the system, generating auxiliary assertions; the top-down method performs an abstract backward propagation to strengthen given properties. Exact application of these methods is complete but is usually infeasible for large-scale verification. Approximation techniques are often needed to complete the verification. We give an overview of known methods for generation of auxiliary invariants in the verification of invariance properties. We extend these methods, by formalizing and analyzing a general verification rule that uses assertion graphs to generate auxiliary assertions for the verification of general safety properties.
引用
收藏
页码:49 / 87
页数:39
相关论文
共 17 条
[1]
BENSALEM S, 1996, LECT NOTES COMPUTER, V1102, P323
[2]
BJORNER NS, 1995, STANCSTR951562 STANF
[3]
BJORNER NS, 1995, LNCS, V976, P589
[4]
ON THE MECHANICAL DERIVATION OF LOOP INVARIANTS [J].
CHADHA, R ;
PLAISTED, DA .
JOURNAL OF SYMBOLIC COMPUTATION, 1993, 15 (5-6) :705-744
[5]
COUSOT P, **DROPPED REF**
[6]
Cousot P, 1977, POPL, P238, DOI DOI 10.1145/512950.512973
[7]
DILL D, 1995, LECT NOTES COMPUTER, P409
[8]
German S. M., 1975, IEEE Transactions on Software Engineering, VSE-1, P68, DOI 10.1109/TSE.1975.6312821
[9]
HAREL D, 1984, CS8405 WEIZM I SCI D
[10]
HEINTZE N, 1992, THESIS CARNEGIEMELLO