Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas' Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.

Eventual Linear Ranking Functions / Bagnara, Roberto; Mesnard, F.. - (2013), pp. 229-238. (Intervento presentato al convegno 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013) tenutosi a Madrid, Spagna nel September 16-18, 2013) [10.1145/2505879.2505884].

Eventual Linear Ranking Functions

BAGNARA, Roberto;
2013-01-01

Abstract

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas' Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.
2013
9781450321549
Eventual Linear Ranking Functions / Bagnara, Roberto; Mesnard, F.. - (2013), pp. 229-238. (Intervento presentato al convegno 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013) tenutosi a Madrid, Spagna nel September 16-18, 2013) [10.1145/2505879.2505884].
File in questo prodotto:
File Dimensione Formato  
ppdp13.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 276.55 kB
Formato Adobe PDF
276.55 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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2631458
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 19
  • ???jsp.display-item.citation.isi??? ND
social impact