The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers.
A New Look at the Automatic Synthesis of Linear Ranking Functions / Bagnara, Roberto; Mesnard, F.; Pescetti, Andrea; Zaffanella, Enea. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 215:(2012), pp. 47-67. [10.1016/j.ic.2012.03.003]
A New Look at the Automatic Synthesis of Linear Ranking Functions
BAGNARA, Roberto;PESCETTI, ANDREA;ZAFFANELLA, Enea
2012-01-01
Abstract
The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers.File | Dimensione | Formato | |
---|---|---|---|
IC_C3800.pdf
non disponibili
Tipologia:
Documento in Pre-print
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
463.08 kB
Formato
Adobe PDF
|
463.08 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.