Paper Info
Title
Transition invariants and transition predicate abstraction for program termination
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-19835-9_2
TACAS
Keywords
Field
DocType
concurrent program,transition predicate abstraction,proof rule,underlying principle,transition invariants,fairness assumption,abstraction-based algorithm,program termination,liveness property,sequential program,specialized setting
Discrete mathematics,Abstraction,Programming language,Predicate abstraction,Computer science,Theoretical computer science,Invariant (mathematics),Liveness
Conference
Volume
ISSN
Citations 
6605
0302-9743
6
PageRank 
References 
Authors
0.46
3
2
Name
Order
Citations
PageRank
Andreas Podelski12760197.87
Andrey Rybalchenko2143968.53