Transition Invariants and Transition Predicate Abstraction for Program Termination

被引：0

作者：

Podelski, Andreas ^{[1
]}

Rybalchenko, Andrey ^{[2
]}

机构：

[1] Univ Freiburg, Freiburg, Germany

[2] Tech Univ Munich, Munich, Germany

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS | 2011年 / 6605卷

关键词：

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Originally, the concepts of transition invariants and transition predicate abstraction were used to formulate a proof rule and an abstraction-based algorithm for the verification of liveness properties of concurrent programs under fairness assumptions. This note applies the two concepts for proving termination of sequential programs. We believe that the specialized setting exhibits the underlying principles in a more direct way.

引用

页码：3 / +

页数：3

共 50 条

[21] Stochastic individual predicate/transition nets
Yao YUE
Journal of Zhejiang University(Science A:An International Applied Physics & Engineering Journal), 2009, 10 (02) : 165 - 171
[22] Stochastic individual predicate/transition nets
Yue, Yao
Zhang, Chun-ming
Wang, Hai-xin
Bai, Guo-qiang
Chen, Hong-yi
JOURNAL OF ZHEJIANG UNIVERSITY-SCIENCE A, 2009, 10 (02): : 165 - 171
[23] Ranking abstraction as companion to predicate abstraction
Balaban, I
Pnueli, A
Zuck, LD
FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 1 - 12
[24] Ranking abstraction as a companion to predicate abstraction
Pnueli, A
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2005, 3707 : 1 - 1
[25] Polymorphic predicate abstraction
Ball, T
Millstein, T
Rajamani, SK
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005, 27 (02): : 314 - 343
[26] PARAMETERIZED REACHABILITY TREES FOR PREDICATE TRANSITION NETS
LINDQVIST, M
ACTA POLYTECHNICA SCANDINAVICA-MATHEMATICS AND COMPUTER SCIENCE SERIES, 1989, (54): : 1 - 120
[27] A METHODOLOGY FOR CONSTRUCTING PREDICATE TRANSITION NET SPECIFICATIONS
HE, XD
LEE, JAN
SOFTWARE-PRACTICE & EXPERIENCE, 1991, 21 (08): : 845 - 875
[28] Compositional semantics for unmarked predicate/transition nets
Schettini, A.Maggiolo
Pina, G.M.
Winkowski, J.
Fundamenta Mathematicae, 1991, 14 (01) : 109 - 128
[29] Predicate abstraction in protocol verification
Pek, E
Bogunovic, N
CONTEL 2005: PROCEEDINGS OF THE 8TH INTERNATIONAL CONFERENCE ON TELECOMMUNICATIONS, VOLS 1 AND 2, 2005, : 627 - 632
[30] A symbolic approach to predicate abstraction
Lahiri, SK
Bryant, RE
Cook, B
COMPUTER AIDED VERIFICATION, 2003, 2725 : 141 - 153

← 1 2 3 4 5 →