CMP.13:11 - SoTA-Echoing

How can a cheaper computation answer a selected question about executions? Adopt the calculational approach organized in Cousot’s Principles of Abstract Interpretation: choose the property semantics and derive effective abstract operations. Its scope includes dataflow, dependency and typing as well as numerical properties. This changes :4.1–4.3 from selecting a convenient picture to constructing a sound obtaining procedure. Direct finite exploration remains a serious cheaper alternative when its state space is manageable; a changed property or obtaining cost reopens the choice.

When independent summaries lose a needed relation, adapt the combination of algebraic and logical abstractions in Cousot, Cousot and Mauborgne, especially their sound-transformer and reduced-product constructions. Combine complementary restrictions when that recovers the answer more cheaply than one uniformly rich domain. Solver-backed relations accept solver and representation costs; simple precomputed operations accept reduced expressiveness. The paper’s implementation comparisons are historical, not a ranking of current tools. The choice changes :4.2 and :4.5 and is reopened by a relevant lost correlation or unsupported machine semantics.

For a reported abstract counterexample, adopt the reconstruct-and-refine step from Clarke and colleagues, sections 4.3–4.4. Its finite-path construction motivates :4.4–4.5 and :5.1: split the distinction that prevents consecutive realization. Uniformly increasing precision is the rival; it can resolve more future questions but pays for distinctions this path may not need. Infinite-path properties require the additional loop conditions rather than reuse of the finite-path test alone.

How should cyclic abstract computations be scheduled? Adapt the question raised by Yang and colleagues’ 2025 interprocedural ordering method: distinguish actual recursive dependencies from spurious cycles introduced by merged call contexts, then choose where widening and narrowing operate. This strengthens :4.3’s dependency-sensitive choice. A simple global worklist remains suitable when it produces an adequate result at lower construction cost. The reported advantages concern the paper’s recursive-program analyses; they do not establish a universal schedule for every abstract domain. Lost call correlation or iteration cost can trigger reconsideration.