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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Computing Herbrand equivalences of terms in data flow frameworks is well studied in program analysis. While algorithms use iterative fix-point computation on some abstract lattice of expressions relevant to the flow graph, the definition of Herbrand equivalences is based on an equivalence over all program paths formulation, on the (infinite) set of all expressions. The aim of this paper is to develop a lattice theoretic fix-point formulation of Herbrand equivalence on a concrete lattice defined over the set of all terms constructible from variables, constants and operators of a program. This new formulation makes explicit the underlying lattice framework as well as the monotone function involved in computing Herbrand equivalences. We introduce the notion of Herbrand congruence and define an (infinite) concrete lattice of Herbrand congruences. Herbrand equivalence is defined as the maximum fix-point of a composite transfer function defined over an appropriate product lattice of the above concrete lattice. We then re-formulate the traditional meet over all paths definition in our lattice theoretic framework. and prove that the maximum fix-point (MFP) and the meet-over-all-paths (MOP) formulations coincide as expected.

A Fix-Point Characterization of Herbrand Equivalence of Expressions in Data Flow Frameworks