Ranking Abstractions

Abstractions Aziem Chawdhary1 , Byron Cook2 , Sumit Gulwani2 , Mooly Sagiv3 , and Hongseok Yang1 1 Queen Mary, University of London 2 Microsoft Research 3 Tel Aviv University Abstract. We propose an abstract interpretation algorithm for proving that a prominates on all inputs. The algorithm uses a novel abstract domain which uses ranking relations to conservatively represent relations between intermediate states. One of the attractive aspects of the algorithm is that it abstracts information that is usually not important for proving termination such as program invariants and yet it distinguishes between different reasons for termination which usually maintained in existing abstract domains. We have implemented a prototype of the algorithm and shown that in practice it is fast and precise.

• Type: Conference
• Year: 2008
• Where: ESOP
• Authors: Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang
• Keywords: Abstract Domains, Abstract Interpretation Algorithm, ESOP 2008, Programming Languages, Tel Aviv University