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 条
  • [1] Transition predicate abstraction and fair termination
    Podelski, Andreas
    Rybalchenko, Andrey
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2007, 29 (03):
  • [2] Transition predicate abstraction and fair termination
    Podelski, A
    Rybalchenko, A
    ACM SIGPLAN NOTICES, 2005, 40 (01) : 132 - 144
  • [3] Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction
    Zuleger, Florian
    STATIC ANALYSIS (SAS 2018), 2018, 11002 : 423 - 444
  • [4] Termination Analysis with Compositional Transition Invariants
    Kroening, Daniel
    Sharygina, Natasha
    Tsitovich, Aliaksei
    Wintersteiger, Christoph M.
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 89 - +
  • [5] Size-Change Termination and Transition Invariants
    Heizmann, Matthias
    Jones, Neil D.
    Podelski, Andreas
    STATIC ANALYSIS, 2010, 6337 : 22 - +
  • [6] Constructing quantified invariants via predicate abstraction
    Lahiri, SK
    Bryant, RE
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2004, 2937 : 267 - 281
  • [7] Predicate Abstraction in a Program Logic Calculus
    Weiss, Benjamin
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2009, 5423 : 136 - 150
  • [8] Efficient Predicate Abstraction of Program Summaries
    Gurfinkel, Arie
    Chaki, Sagar
    Sapra, Samir
    NASA FORMAL METHODS, 2011, 6617 : 131 - 145
  • [9] Effective predicate abstraction for program verification
    Li, Li
    Gu, Ming
    Song, Xiaoyu
    Wang, Jianmin
    TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 129 - +
  • [10] Predicate abstraction in a program logic calculus
    Weiss, Benjamin
    SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (10) : 861 - 876
12345