Abstract Interpretation, Type Systems, and Verified Static Analysis

Testing the command below at inputs $0,1,2$ reveals three traces. Its input, however, ranges over all natural numbers, and its loop makes the set of reachable states infinite. The collecting semantics records exactly every execution, but computing it is as hard as executing every input. A sound static analyzer must forget enough to terminate and remember enough to justify its alarms. The analyzer below is derived from those two obligations rather than presented as an oracle, following the fixed-point view that founded abstract interpretation [CC77].

Concrete and collecting semantics

Let variables range over a finite set $\mathsf{Var}$, integers over $\mathbb{Z}$, and stores over total maps $\sigma :\mathsf{Var}\to \mathbb{Z}$. Expressions, tests, and commands are A strict comparison abbreviates negated non-strict comparison; in particular, means $\mathrm{\neg }(x\le 0)$. The opening $x:={\mathsf{input}}_{\mathbb{N}}$ is metanotation for the initial store family $I=\{⟨c,{\sigma }_n⟩\mid n\in \mathbb{N},{\sigma }_n(x)=n\}$, not an extra command constructor. A configuration is $⟨c,\sigma ⟩$ or the terminal state $\mathsf{error}$. The deterministic small-step rules are the usual rules for assignment, sequencing, conditionals, and loop unfolding. An assertion steps to $⟨\mathbf{skip},\sigma ⟩$ when its test is true and to $\mathsf{error}$ otherwise. The input command is represented by the initial set of stores; it is not a nondeterministic expression in later states.

For input $2$, the loop-head projections are and both loop assertions hold at the first two visits. The last assertion holds at the third. This finite trace is a calculation, not the general safety proof.

Proof of Theorem 68.2 — Fixed-point characterization of reachability

Proof. If $X\subseteq Y$, every predecessor chosen from $X$ is also in $Y$; hence ${\mathcal{F}}_{c_0}(X)\subseteq {\mathcal{F}}_{c_0}(Y)$. Knaster–Tarski therefore supplies a least fixed point. Let $$R_n=\{\kappa \mid \mathrm{\exists }{\kappa }_0\in I.{\kappa }_0{⟶}^{\le n}\kappa \}.$$ Induction on $n$ gives ${\mathcal{F}}_{c_0}^{n+1}(\varnothing )=R_n$. Their union is closed under one step and contains $I$, so it is a fixed point. Every pre-fixed point containing $I$ contains every $R_n$, by the same induction. The union is therefore least. This uses only the powerset instance of the fixed-point machinery developed in chapter 12. ◻

A first abstraction: signs

Let $$\mathsf{Sgn}:=\mathcal{P}(\{-,0,+\})$$ ordered by inclusion. Bottom is the empty set and top is $\{-,0,+\}$. For $Z\subseteq \mathbb{Z}$, define An abstract store maps each variable to a sign set. Its concretization is pointwise.

Proof of Lemma 68.3 — Sign Galois insertion

Proof. Both directions unfold to $\mathrm{\forall }n\in Z.\mathrm{sgn}(n)\in S$. For the insertion equation, every sign has a representative integer: $-1,0,1$. ◻

Define abstract addition by joining all possible sign-table entries: $$S_1{+}^{\mathrm{♯}}{S}_2=\{\mathrm{sgn}(m+n)\mid \mathrm{sgn}(m)\in S_1,\mathrm{sgn}(n)\in S_2\}.$$ Subtraction is addition after sign reversal. A test refines the store by removing sign combinations that cannot satisfy it. When signs alone cannot decide a comparison between two non-singleton variables, both branches remain.

Proof of Lemma 68.4 — Local soundness of signs

Proof. Induct on $e$. Constants and variables follow from the definitions. For addition, the two induction hypotheses put the operands in sign classes enumerated by ${+}^{\mathrm{♯}}$, so their concrete sum is included. Subtraction is identical after reversal. The test claim follows by inspecting the retained sign pairs; an undecidable pair is deliberately kept on both sides. ◻

At the first loop head of $\mathsf{Countdown}$, signs infer $$x\mapsto \{-,0,+\},y\mapsto \{0,+\}.$$ The true guard refines $x$ to $\{+\}$, but the sign table for subtracting the positive constant $1$ must still contain all three signs. Joining the back edge therefore makes $x$ top. Signs prove $0\le y$, but prove neither $0\le x$ nor $x\le y$. These are false alarms caused by forgotten magnitude and relation, not unsound results.

Galois connections package sound approximation

Proof of Lemma 68.6 — Consequences of the adjunction

Proof. Put $a=\alpha (c)$ and use reflexivity for extensiveness. Put $c=\gamma (a)$ for reductiveness. If $c⊑c^{\prime }$, then $c⊑c^{\prime }⊑\gamma \alpha (c^{\prime })$, so the correspondence gives $\alpha (c)⊑\alpha (c^{\prime })$; the proof for $\gamma$ is dual. Compose extensiveness and reductiveness with monotonicity to obtain both idempotence equations. ◻

Proof of Theorem 68.7 — Best correct approximation

Proof. Extensiveness at $F(\gamma (a))$ gives $$F\gamma (a)⊑\gamma \alpha F\gamma (a).$$ For optimality, soundness of $G$ says $F\gamma (a)⊑\gamma G(a)$. The adjunction moves this inequality across $\alpha ⊣\gamma$, yielding $\alpha F\gamma (a)⊑G(a)$. ◻

Best does not mean complete. It means most precise among sound functions on the selected abstract domain. A coarser domain can have a best transformer and still lose the invariant needed by a client.

Intervals and compositional transformers

Let lower bounds range over $\mathbb{Z}\cup \{-\mathrm{\infty }\}$ and upper bounds over $\mathbb{Z}\cup \{+\mathrm{\infty }\}$. The interval domain consists of bottom and pairs $[l,u]$ with $l\le u$, ordered by inclusion of their integer meanings: $${\gamma }_{\mathsf{i}}([l,u])=\{n\in \mathbb{Z}\mid l\le n\le u\}.$$ The abstraction of a nonempty integer set is its least enclosing extended interval; the empty set maps to bottom.

Proof of Lemma 68.8 — Interval Galois insertion

Proof. The hull of $Z$ lies within $[l,u]$ exactly when every member of $Z$ lies between $l$ and $u$. Taking the hull of all integers in an interval recovers its endpoints; bottom is immediate. ◻

Interval addition and subtraction are where a lower-bound calculation containing $-\mathrm{\infty }$ yields $-\mathrm{\infty }$, and an upper-bound calculation containing $+\mathrm{\infty }$ yields $+\mathrm{\infty }$. The separated endpoint sets ensure that no indeterminate $+\mathrm{\infty }+(-\mathrm{\infty })$ case occurs. A true filter for replaces the upper bound of $x$ by $min(u_x,n-1)$; the false filter replaces its lower bound by $max(l_x,n)$. Empty results become bottom.

Proof of Theorem 68.10 — Compositional analyzer soundness

Proof. Induct on the syntax of $c$. Assignment uses expression soundness. Sequencing composes the two induction hypotheses. A conditional uses the sound refinement corresponding to the concrete Boolean and then the selected branch hypothesis. Assertion soundness follows because a concrete false state is retained by the false refinement, so its nonbottom test sets the flag. For sequencing, an error occurs either in the first command or in the second from a terminal first-command store, exactly matching the disjunction. For a loop, induction on the number of completed iterations shows that every loop-head store lies in every pre-fixed point $X$ satisfying ${\mathrm{\Phi }}_A(X)⊑X$; leastness puts it in the selected invariant. The exit filter handles a terminal failed guard and the body flag handles an assertion error during an iteration. ◻

For $\mathsf{Countdown}$, interval filtering gives at the loop head $$x\mapsto [0,+\mathrm{\infty }],y\mapsto [0,+\mathrm{\infty }].$$ The transfer $x:=x-1$ followed by the loop-head filter restores the same invariant. The analyzer proves the first assertion and, at loop exit, refines $x$ to $[0,0]$, proving the final assertion. Like signs, it cannot prove the relational assertion $x\le y$.

Fixed-point transfer, widening, and narrowing

Proof of Theorem 68.11 — Fixed-point transfer

Proof. The abstract least fixed point is a fixed point, so soundness gives $$F(\gamma (\mathrm{lfp}{F}^{\mathrm{♯}}))⊑\gamma (F^{\mathrm{♯}}(\mathrm{lfp}{F}^{\mathrm{♯}}))=\gamma (\mathrm{lfp}{F}^{\mathrm{♯}}).$$ Thus its concretization is a pre-fixed point of $F$. Leastness of $\mathrm{lfp}(F)$ gives the result. ◻

Exact interval iteration need not terminate. The commands $$x:=0;\mathbf{while}\mathsf{true}\mathbf{do}x:=x+1$$ generate $$[0,0]⊏[0,1]⊏[0,2]⊏\cdots .$$

Proof of Theorem 68.13 — Widening coverage and termination

Proof. Each widened endpoint either stays fixed or moves once to its corresponding infinity. With finitely many program variables, only finitely many such moves exist, so the sequence stabilizes. Coverage is immediate from the two endpoint cases. At stability, $$A_N=A_N\mathrm{\nabla }{F}^{\mathrm{♯}}(A_N)$$ and coverage gives $F^{\mathrm{♯}}(A_N)⊑A_N$. Soundness and monotonicity of $\gamma$ give $$F(\gamma A_N)⊑\gamma (F^{\mathrm{♯}}{A}_N)⊑\gamma A_N.$$ Thus $\gamma A_N$ is a concrete pre-fixed point. Park induction—leastness of $\mathrm{lfp}(F)$ among pre-fixed points—gives the second claim. ◻

A selected interval endpoint replacement narrows an infinite endpoint to the corresponding finite endpoint proposed by $F^{\mathrm{♯}}(A)$, leaving finite endpoints unchanged. This chapter applies a narrowing step only when a subsequent check confirms $F^{\mathrm{♯}}(A^{\prime })⊑A^{\prime }$. That check preserves soundness. Without that check, this particular endpoint replacement has no soundness theorem. Standard narrowing operators instead carry their own coverage and descending-chain conditions; those conditions are not claimed for this deliberately small operator.

A relational refinement

Independent intervals cannot remember that the initialization $y:=x$ makes $x\le y$, nor that decrementing only $x$ preserves it. Add difference constraints $$u-v\le k$$ over program variables and a distinguished zero variable. A relational abstract store is a difference-bound matrix $D$; its concretization contains the stores satisfying every finite entry. Assignment by a copy plus a constant updates both the row and column for the assigned variable. For every variable or distinguished zero node $w$, before closure, Closure then composes bounds by the triangle inequality. Forgetting either the row or the column is not an assignment transformer.

Proof of Lemma 68.14 — Sound reduction with intervals

Proof. Each tightening is a logical consequence of constraints already present in the other component. It therefore removes no concrete store from the intersection. Conversely, tightening only removes stores that violated such a consequence, so it adds none. Apply any finite schedule of these closure and propagation rules; equality of concretizations is preserved at every step. This lemma claims semantic preservation, not termination of an unrestricted alternating saturation procedure. ◻

At entry to the loop of $\mathsf{Countdown}$, the matrix contains $x-y\le 0$ and $y-x\le 0$. The assignment $x:=x-1$ changes these to $x-y\le -1$ and $y-x\le 1$. Joining loop iterations preserves $$x-y\le 0,$$ but the reverse bound grows through $1,2,\dots$. The loop solver therefore widens DBM entries: a bound that weakens is replaced by $+\mathrm{\infty }$, while a stable or strengthening bound is retained, followed by closure. Each of the finitely many entries is dropped at most once, so the iteration terminates. For this loop, $y-x$ is dropped and $x-y\le 0$ remains. The latter is inductive and proves the relational assertion. Together with the interval facts $x,y\ge 0$, it proves that no assertion in $\mathsf{Countdown}$ can reach $\mathsf{error}$.

Proof of Corollary 68.15 — Countdown safety

Proof. The interval–difference reduced product establishes the inductive loop invariant $$0\le x,0\le y,x\le y.$$ Local assertion soundness excludes the two loop errors. The false loop guard and $0\le x$ imply $x=0$, excluding the final error. ◻

A bounded borrow-graph case

Move’s reference-safety analysis supplies a less numerical instance of the same design. An abstract location names a local variable or operand-stack slot. A path is a finite field sequence, optionally ending in $\ast$ to denote all extensions. An edge $$\mathsf{Borrow}(m,p,n)$$ says that the reference at $n$ is borrowed from the location reached by path $p$ from $m$. Eliminating a temporary node composes every incoming edge with every outgoing edge before deleting the node; a field borrow extends the edge label. These operations deliberately forget concrete addresses but retain the rooted-path relation needed after a temporary is popped.

The abstract program annotation is computed by a forward fixed point. Its order keeps local and stack types equal and permits each borrow edge in the smaller graph to be subsumed by an edge in the larger graph. Transfer rejects a move or overwrite when an outgoing edge witnesses a live borrow. The soundness relation $\mathsf{Inv}(s,\hat{s})$ packages four obligations: type agreement, no leaked allocated location, every reference rooted by a realized acyclic borrow path, and referential transparency for mutation.

Proof of Theorem 68.16 — Move borrow-graph preservation

Proof. This is Theorem 1 and its stated corollary in the frozen Move borrow-checker paper, at printed pages 8–9 [BMNQ22]. The source proof decomposes the step into a local abstract transition, proves that transition preserves $\mathsf{Inv}$, and then uses annotation subsumption to reach the fixed-point annotation at the successor program counter. We import that theorem only at its bytecode, abstraction, and invariant signature. It is not a theorem about the place calculus of chapter 48 or about the interval analyzer above, and the archived implementation is evidence of lineage rather than a machine-checked refinement proof. ◻

A type system as an abstract semantics

Use a separate call-by-value expression language $$e::=n\mid \mathsf{true}\mid \mathsf{false}\mid x\mid e+e\mid \lambda x.e\mid ee,$$ with integer, Boolean, and closure values. This is not an instance of the first-order command semantics above. Interpret simple types as sets of values: $$\gamma (\mathsf{Int})=\mathbb{Z},\gamma (\mathsf{Bool})=\{\mathsf{true},\mathsf{false}\}.$$ The arrow interpretation is The arrow clause is a partial-correctness abstraction: it constrains every terminating application and does not assert termination. The sound abstract addition transformer accepts $\mathsf{Int}\times \mathsf{Int}$ and returns $\mathsf{Int}$; application accepts $(A\to B)\times A$ and returns $B$. Writing these transfer conditions as judgments gives the usual variable, integer, Boolean, addition, abstraction, and application rules. In particular, $$\frac{\mathrm{\Gamma },x:A⊢e:B}{\mathrm{\Gamma }⊢\lambda x.e:A\to B}\mathrm{Ty}-\mathrm{Abs}\frac{\begin{array}{c}\mathrm{\Gamma }⊢e_1:A\to B\\ \mathrm{\Gamma }⊢e_2:A\end{array}}{\mathrm{\Gamma }⊢e_1{e}_2:B}\mathrm{Ty}-\mathrm{App}.$$

Proof of Theorem 68.17 — Type safety from abstraction

Proof. Induct on the typing derivation together with the terminating evaluation. Variables use the environment hypothesis. Addition inverts both premises to integer denotations, so the primitive is defined and returns an integer. For Ty-Abs, the resulting closure satisfies the displayed universal condition by the induction hypothesis for the body. For Ty-App, the operator induction hypothesis supplies a closure in $\gamma (A\to B)$, the operand hypothesis supplies an argument in $\gamma (A)$, and the arrow condition gives the result in $\gamma (B)$. These cases cover every primitive that can raise a tag error. ◻

This is type-system soundness, proved for the expression semantics just defined. It does not imply completeness: after adding conditionals, $\mathbf{if}\mathsf{true}\mathbf{then}0\mathbf{else}\mathsf{false}$ evaluates safely but has no simple type. It does not imply principality either: that property requires type variables and an instantiation relation, neither of which this monomorphic fragment contains. A union or singleton-refinement domain may type more safe terms, which is a precision or completeness change rather than a principality theorem. Command-analyzer soundness, type-system soundness, completeness, and principality are separate statements. The general derivation of types as abstract interpretations belongs to Cousot’s exact framework [Cou97]; the local theorem above needs only the displayed tag abstraction.

Higher-order analysis by abstracting a machine

A CEK state $$⟨e,\rho ,\kappa ⟩$$ contains an expression, an environment from variables to closures, and a continuation. For the expression language of section 68.8, use frames $$\kappa ::=\mathsf{mt}\mid \mathsf{ar}(e,\rho ,\kappa )\mid \mathsf{fn}(v,\kappa ),$$ and the representative rules $$\frac{\phantom{X}}{⟨e_0{e}_1,\rho ,\kappa ⟩⟶⟨e_0,\rho ,\mathsf{ar}(e_1,\rho ,\kappa )⟩}\mathrm{CEK}-\mathrm{App}$$ $$\frac{v_0\mathsf{value}}{⟨v_0,\rho ,\mathsf{ar}(e_1,{\rho }_1,\kappa )⟩⟶⟨e_1,{\rho }_1,\mathsf{fn}(v_0,\kappa )⟩}\mathrm{CEK}-\mathrm{Arg}$$ $$\frac{v_1\mathsf{value}}{⟨v_1,{\rho }_1,\mathsf{fn}(⟨\lambda x.e,{\rho }_0⟩,\kappa )⟩⟶⟨e,{\rho }_0[x\mapsto v_1],\kappa ⟩}\mathrm{CEK}-\mathrm{Beta}.$$ Variable lookup replaces $x$ by the closure $\rho (x)$; integer primitives add explicit left- and right-operand frames of the same shape. Recursive environments and continuations make the reachable state space infinite even for one finite program. The route to a finite analysis is operational.

First store-allocate bindings: $$\rho :\mathsf{Var}\to \mathsf{Addr},\sigma :\mathsf{Addr}\to \mathcal{P}(\mathsf{Closure}).$$ Then store-allocate continuation tails as storable values. Add a finite time component and parameterize the machine by $$\mathsf{tick}:{\mathrm{\Sigma }}^{\mathrm{♯}}\to {\mathsf{Time}}^{\mathrm{♯}},\mathsf{alloc}:{\mathrm{\Sigma }}^{\mathrm{♯}}\to {\mathsf{Addr}}^{\mathrm{♯}}.$$ The abstract address and time sets are finite. Reusing an address changes store overwrite to join, and lookup becomes nondeterministic over every value in the stored set. Syntax is finite for the analyzed program; the remaining state components are finite maps over finite sets. Reachability is therefore decidable.

Fix maps ${\alpha }_a$ and ${\alpha }_t$ from concrete addresses and times to their finite counterparts. Abstraction maps an environment pointwise through ${\alpha }_a$; at an abstract address $\hat{a}$, it joins all closures and continuation tails stored at concrete addresses mapped to $\hat{a}$. Abstract states are ordered by equality on control expression and environment, and subset inclusion at every store address. The parameter contracts are $$\begin{array}{}\text{(}Machine-Parameters\text{)}& {\alpha }_t(\mathsf{tick}(\varsigma ))=\widehat{\mathsf{tick}}(\alpha \varsigma ),{\alpha }_a(\mathsf{alloc}(\varsigma ))=\widehat{\mathsf{alloc}}(\alpha \varsigma ).\end{array}$$ Allowing inclusion instead of equality yields the same simulation after choosing a related abstract address or time.

Proof of Theorem 68.18 — Abstract-machine simulation

Proof. Proceed by cases on the displayed CEK rules and their store-allocated counterparts. Variable lookup is included because the abstract store entry contains the abstraction of the concrete closure. In CEK-App, storing the continuation tail at the concrete allocation maps to the address selected by the abstract allocation equation; store join retains that tail and any old occupants. CEK-Arg changes only the finite frame payload. In CEK-Beta, the argument closure is joined at the allocated binding address and the abstract environment points to it. Return does the same for a store-allocated continuation. All control expressions and environments commute with $\alpha$, while the tick equation relates successor times. Selecting the joined occupant that abstracts the concrete one supplies the required nondeterministic successor. Integer-frame cases repeat the CEK-Arg argument and variable lookup uses the defining store union. ◻

This is the CESK-star simulation pattern of Van Horn and Might, whose exact Theorem 2 states the same one-step obligation after store allocation and finite-address abstraction [VHM12]. Allocation policy controls precision: one address per variable gives a monovariant analysis; including a bounded call string distinguishes contexts. No theorem from the control calculi of chapter 17 is transferred here.

Constructive Galois connections and extraction

A classical powerset abstraction $\alpha :\mathcal{P}(C)\to A$ may be noncomputable even when the resulting analyzer is executable. A constructive Galois connection separates the pure calculation from the specification effect.

Proof of Lemma 68.20 — Constructive calculation of a transformer

Proof. Take $c\in \mu (a)$. The correspondence gives $\eta (c)⊑a$. Monotonicity of $f^{\mathrm{♯}}$ and the local hypothesis yield $$\eta (f(c))⊑f^{\mathrm{♯}}(\eta (c))⊑f^{\mathrm{♯}}(a).$$ Apply the correspondence in reverse. ◻

For the binary form used in arithmetic, take $c_i\in \mu (a_i)$. The correspondence and monotonicity in the two coordinates give the complete calculation $$\eta (g(c_1,c_2))⊑g^{\mathrm{♯}}(\eta (c_1),\eta (c_2))⊑g^{\mathrm{♯}}(a_1,a_2).$$ Applying the correspondence in reverse therefore proves the following instance. If $g:C\times C\to C$, $g^{\mathrm{♯}}:A\times A\to A$ is monotone in both arguments, and $\eta (g(c_1,c_2))⊑g^{\mathrm{♯}}(\eta c_1,\eta c_2)$, then $$g(\mu (a_1)\times \mu (a_2))\subseteq \mu (g^{\mathrm{♯}}(a_1,a_2)).$$

For intervals, $\eta (n)=[n,n]$ and $\mu ([l,u])=\{n\mid l\le n\le u\}$. Calculating addition through lemma 68.20 yields the executable endpoint function, while the set image remains in the proof. Darais and Van Horn’s constructive framework mechanizes this separation and its calculational rules in Agda [DVH19]. The pinned artifact is evidence for that formalization; it is not silently imported as the proof of this chapter’s imperative analyzer.

Proof of Theorem 68.21 — Extracted analyzer boundary

Proof. Every named component except the specification relation is defined by structural recursion or a finite worklist; widening supplies termination for the interval product, and DBM extrapolation drops each unstable entry at most once. Lemma 68.20 eliminates the specification effect at primitive transformers; theorem 68.10, theorem 68.13 compose the resulting local simulations and justify checked loop invariants. Difference-bound reduction is sound by lemma 68.14. Erasing proofs therefore leaves only the pure functions. The Kappa artifact checks selected interval, widening, and relational calculations on one finite trace; it is not the extracted analyzer asserted by this theorem. ◻

A verified analyzer trust case

Verasco analyzes C$\mathrm{\#}$minor, an intermediate language immediately before CompCert’s Cminor. Its concrete semantics is continuation-based small-step execution. Its state abstraction combines local and memory environments, nonrelational and relational numerical domains, congruences, intervals, floating-point bounds, and a memory abstraction. Domain interfaces are written in $\gamma$-only form: each operation carries a theorem that its concrete inputs and outputs lie in the concretization. This avoids computing a powerset abstraction inside Coq.

Loops and gotos are solved by a structural interpreter and pre-fixed-point iteration. Widening and narrowing use explicit fuel. The paper discusses an untrusted iterator whose candidate would be accepted only by a verified checker, but the exact theorem imported below is for the pinned implemented pipeline, not for that alternative architecture. The polyhedral component locally uses certificates checked by verified code. The extracted OCaml analyzer is linked with CompCert’s verified front end and compiler; the OCaml runtime and extraction mechanism remain outside the Coq kernel.

Proof of Theorem 68.22 — Verasco's exact safety conclusion

Proof. This is the paper’s final Coq theorem vanalysis_correct, imported at its C$\mathrm{\#}$minor signature [JLB^+15]. The proof factors through the verified C$\mathrm{\#}$minor program logic, sound abstract-domain interfaces, and checked pre-fixed points. CompCert semantics preservation transfers the established safety property to generated assembly. The theorem does not claim absence of alarms, functional correctness, termination, or correctness of unverified performance heuristics rejected by their checkers. ◻

Paths are not traces

Consider $$\begin{array}{l}\mathbf{if}x=0\mathbf{then}y:=0\mathbf{else}y:=1;\\ \mathbf{if}y=0\mathbf{then}\mathbf{assert}x=0\mathbf{else}\mathbf{skip}.\end{array}$$ A syntactic control-flow path records the chosen edges and composed transfer functions. A semantic trace also records the stores that make those edges feasible and the values computed along them. The apparent path combining the first else edge $x\ne 0$ with the later then edge $y=0$ is syntactically describable but semantically infeasible: the first edge assigns $y=1$.

Proof of Proposition 68.24 — Neither target is a renaming of the other

Proof. The displayed program supplies the first claim. Joining after the first conditional gives $x\mapsto [-\mathrm{\infty },+\mathrm{\infty }]$ and $y\mapsto [0,1]$; filtering the second then edge leaves $x$ unconstrained, so an interval analysis cannot prove its assertion. Every semantic trace taking that edge came from the first then branch and has $x=0$. Thus the infeasible combination contributes to the joined path state but to no trace. For the second claim, alter an assignment edge transformer so that it leaves the abstract state unchanged. The equations still describe their own syntactic paths, but the concrete assignment changes the store and violates transition simulation. ◻

Cousot’s structural trace development derives the two specifications from different abstractions and exhibits examples involving liveness and deadness where a syntactic statement does not establish the intended semantic property [Cou19]. We use that result only for this distinction; it does not replace the compositional soundness theorem proved above.

A source-gated probabilistic application

The interval-trace semantics of Beutner, Ong, and Zaiser assigns each finite interval trace $\mathit{t}=⟨[a_1,b_1],\dots ,[a_n,b_n]⟩$ a volume $\mathrm{vol}(\mathit{t})=\prod _i(b_i-a_i)$, an interval weight ${\mathsf{wt}}_P^I(\mathit{t})$, and an interval result ${\mathsf{val}}_P^I(\mathit{t})$. Two traces are compatible when some common-coordinate intervals are almost disjoint; a family is compatible when this holds pairwise. A countable family is exhaustive when its cylinders cover almost every infinite sample trace. For measurable $U$, define The brackets are (0/1) indicators.

Proof of Theorem 68.25 — Sound unnormalized measure bounds

Proof. For the lower bound, interval evaluation soundness bounds each concrete trace’s weight below by the interval minimum and its result inside the return interval. Compatibility makes the represented boxes almost disjoint, so their integrals may be summed without double counting. Their union is a subset of all traces, giving the lower inequality.

For the upper bound, interval soundness bounds each represented trace from above. Exhaustivity covers almost every concrete infinite trace, and subadditivity bounds the integral by the sum of interval maxima. These are Theorems 4.1–4.2 of the frozen interval-trace calculus [BOZ22]. We do not import its Theorem 4.3 completeness result. ◻

Posterior bounds additionally require bounds on the normalizing constant and a justified division rule; no normalized claim is made here. This application follows the same approximation pattern, but its concrete objects are measures and traces rather than imperative states. It is static analysis of a probabilistic program, not a semantics-preserving inference transformation.

What the comparisons do and do not identify

Dataflow analysis joins facts at program points. The tag analysis above instead abstracts values and expressions, while the machine abstraction keeps control components explicit. A path-sensitive abstraction may retain guard formulas rather than joining all represented inputs; the two-conditional example in section 68.12 proves that this can be strictly more precise than non-disjunctive intervals. Deductive verification begins from a candidate invariant and checks proof obligations, whereas the analyzer above computes a candidate and then checks the same pre-fixed-point inequality. These are explicit abstraction or algorithmic differences, not a catalogue of systems that happen to share lattice vocabulary.

The chapter’s verified conclusion is narrower and stronger: for the stated integer language, local transformer proofs, fixed-point transfer, widening, checked narrowing, and reduced-product soundness compose into corollary 68.15. Floating point, concurrency, quantitative cost, and arbitrary production analyzers require their own concrete semantics and abstraction proofs.

Chapter seminar

The Kappa corpus at artifacts/ch68-verified-analyzer/ executes the countdown recurrence at input $3$, checks that $[0,3]$ contains both state components along that trace, performs one interval widening and a narrowing proposal checked against the same finite trace, checks $x\le y$ pointwise, and rejects a nonnegative-subtraction claim at $0-1$. It does not implement the sign analyzer, structural command analyzer, or DBM closure. This finite implementation witnesses the displayed calculations; it is not a mechanization of the total theorems or a replay of Verasco.