English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The classical technique for proving termination of a generic sequentialcomputer program involves the synthesis of a ranking function for each loop ofthe program. Linear ranking functions are particularly interesting because manyterminating loops admit one and algorithms exist to automatically synthesizeit. In this paper we present two such algorithms: one based on work dated 1991by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004.Remarkably, while the two algorithms will synthesize a linear ranking functionunder exactly the same set of conditions, the former is mostly unknown to thecommunity of termination analysis and its general applicability has never beenput forward before the present paper. In this paper we thoroughly justify bothalgorithms, we prove their correctness, we compare their worst-case complexityand experimentally evaluate their efficiency, and we present an open-sourceimplementation of them that will make it very easy to includetermination-analysis capabilities in automatic program verifiers.

The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version