Ranking Abstractions

11 years 3 months ago
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.
Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where ESOP
Authors Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang
Comments (0)