Inference of ranking functions for proving temporal properties by abstract interpretation

详细信息    查看全文

• 作者：Caterina Urban^a ; ^b ; ^{caterina.urban@inf.ethz.ch} ; Antoine Miné ; ^a ; ^c ; ^{antoine.mine@lip6.fr}
• 关键词：Static analysis ; Abstract interpretation ; Liveness ; Temporal properties ; Ranking functions ; Termination
• 刊名：Computer Languages, Systems & Structures
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：47
• 期：part_P1
• 页码：77-103
• 全文大小：2036 K
• 卷排序：47

文摘

We present new static analysis methods for proving liveness properties of programs. We generalize an existing abstract interpretation framework for termination. We reuse existing abstract domains based on piecewise-defined ranking functions. The static analyses methods infer sufficient preconditions for the liveness properties. We provide a prototype implementation of these static analyses.