Modular Ranking Abstraction

Ranking Abstraction Ittai Balaban Computer Science Department, New York University, 251 Mercer St., New York, New York 10012, United States and Amir Pnueli Computer Science Department, New York University, 251 Mercer St., New York, New York 10012, United States and Department of Computer Science and Applied Mathematics, The Weizmann Institute of Science, POB 26, Rehovot 76100, Israel and Lenore D. Zuck Department of Computer Science, University of Illinois at Chicago, 851 South Morgan (M/C 152), Room 1120 SEO, Chicago, Illinois 60607, United States Received (received date) Revised (revised date) Communicated by Editor’s name Predicate abstraction has become one of the most successful methodologies for provty properties of programs. Recently, several abstraction methodologies have been for proving liveness properties. This paper studies “ranking abstraction” where a program is augmented by a non-constraining progress monitor based on a set of ranktions, and further abstracted by ...

• Type: Journal
• Year: 2007
• Where: IJFCS
• Authors: Ittai Balaban, Amir Pnueli, Lenore D. Zuck
• Keywords: Abstraction, Computer Science, IJFCS 2007, Ranking