diff --git a/Cslib.lean b/Cslib.lean
index d74457919..79e8f3142 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -2,6 +2,8 @@ module  -- shake: keep-all --deprecated_module: ignore
 
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Analysis.Dataflow.CFG
+public import Cslib.Analysis.Dataflow.Kildall
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic
diff --git a/Cslib/Analysis/Dataflow/CFG.lean b/Cslib/Analysis/Dataflow/CFG.lean
new file mode 100644
index 000000000..317076e09
--- /dev/null
+++ b/Cslib/Analysis/Dataflow/CFG.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Jacopo Moretti. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacopo Moretti
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Fintype.List
+public import Mathlib.Data.Fintype.Sigma
+public import Mathlib.Data.Finset.Sort
+public import Mathlib.Data.DFinsupp.WellFounded
+public import Mathlib.Combinatorics.Quiver.Basic
+public import Mathlib.Combinatorics.Quiver.Covering
+
+
+/-!
+# Control flow graphs
+
+## Main definitions
+
+- `CFG` is a structure representing Control Flow Graphs on which the dataflow
+  algorithm defined in `Kildall.lean` runs.
+-/
+
+@[expose] public section
+
+/-- Abstract structure defining the necessary operations on a CFG to define a Control Flow Graph. -/
+structure CFG where
+  /-- All of the nodes in the CFG. -/
+  Node : Type u
+  /-- A CFG contains a finite amount of nodes. -/
+  [fintypeNode : Fintype Node]
+  /-- An ordering of nodes, to make the conversion to lists computable. -/
+  [orderNode : LinearOrder Node]
+  /-- Decidable equality on nodes. -/
+  [dEqNode : DecidableEq Node]
+  /-- Quiver structure for the edges of the CFG. -/
+  quiver : Quiver Node
+  /-- A CFG contains a finite amount of edges. -/
+  [fintypeEdges : ∀ a b, Fintype (@Quiver.Hom Node quiver a b)]
+  /-- Distinguished entry node in the CFG. -/
+  entry : Node
+
+namespace CFG
+
+instance {g : CFG} : Fintype (g.Node) :=
+  g.fintypeNode
+
+instance {g : CFG} : LinearOrder (g.Node) :=
+  g.orderNode
+
+/-- Finite set of all of the nodes of `g` -/
+def nodesOf (g : CFG) : Finset g.Node := g.fintypeNode.elems
+
+/-- List of all of the nodes of `g`, ordered by the ordering on `g.Node` -/
+def nodeList (g : CFG) : List g.Node := g.nodesOf.sort
+
+/-- Any node of `g` is in `g.nodeList`. -/
+@[simp] theorem mem_nodeList (g : CFG) (n : g.Node) : n ∈ g.nodeList := by
+  rw [nodeList]
+  apply (Finset.mem_sort (· ≤ ·)).mpr
+  exact @Fintype.complete _ g.fintypeNode n
+
+/-- Convenience type for edges of `g`: `Edge src dst` represents an edge between src and dst. -/
+abbrev Edge {g : CFG} (src dst : g.Node) := @Quiver.Hom g.Node g.quiver src dst
+/-- Convenience type for incoming edges of `n` in `g`: `inEdge n` represents the type of edges
+    entering n. -/
+abbrev inEdge {g : CFG} (n : g.Node) := @Quiver.Costar g.Node g.quiver n
+/-- Convenience type for outgoing edges of `n` in `g`: `outEdge n` represents the type of edges
+    entering n. -/
+abbrev outEdge {g : CFG} (n : g.Node) := @Quiver.Star g.Node g.quiver n
+
+/-- All incoming edges of a given node, bundled with their source nodes. -/
+def inEdges {g : CFG} (n : g.Node) : Finset (inEdge n) := by
+  letI := g.quiver
+  letI := g.fintypeNode
+  letI := g.orderNode
+  letI (src dst : g.Node) := g.fintypeEdges src dst
+  exact Finset.univ
+
+/-- All outgoing edges of a given node, bundled with their source nodes. -/
+def outEdges {g : CFG} (n : g.Node) : Finset (outEdge n) := by
+  letI := g.quiver
+  letI := g.fintypeNode
+  letI (src dst : g.Node) := g.fintypeEdges src dst
+  exact Finset.univ
+
+/-- The set of successor nodes of node `n` in `g`. -/
+def succOf {g : CFG} (n : g.Node) : Finset g.Node :=
+  letI := g.dEqNode
+  (outEdges n).image Sigma.fst
+
+end CFG
diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean
new file mode 100644
index 000000000..1f81de052
--- /dev/null
+++ b/Cslib/Analysis/Dataflow/Kildall.lean
@@ -0,0 +1,352 @@
+/-
+Copyright (c) 2026 Jacopo Moretti. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacopo Moretti
+-/
+
+module
+
+public import Cslib.Analysis.Dataflow.CFG
+public import Mathlib.Order.Lattice
+public import Mathlib.Data.DFinsupp.WellFounded
+public import Mathlib.Data.Finset.Sort
+
+/-!
+# Forward Worklist dataflow algorithm
+
+Implementation of Kildall's worklist algorithm for solving dataflow equations, as described in
+@Kildall73. Correctness follows an argument similar to the one found in @Nielson99, with a proof
+technique borrowed from @LaSpina25.
+
+## Main definitions
+
+- `DFState` represents the result of a dataflow analysis algorithm, a mapping between CFG nodes and
+  abstract states.
+- Definitions of correctness (soundness + completeness) for the analysis result, as `Fixpoint`s over
+  the analysis result `ρ`.
+
+## Main theorems
+
+- Termination of the worklist algorithm
+- Correctness of the algorithm : The algorithm computes a postfixpoint.
+- Minimality of the algorithm : The algorithm computes the least solution if the transfer functions
+  are monotone.
+- Correctness of the algorithm : The algorithm computes a fixpoint if the transfer functions are
+  monotone.
+
+## References
+
+* [G. Kildall, *A Unified Approach to Global Program Optimization*][Kildall73]
+* [F. Nielson, H.R. Nielson, C. Hankin, *Principles of Program Analysis*][Nielson99]
+* [R. LaSpina, *Formal Verification of WTO-based Dataflow Solvers*][LaSpina25]
+-/
+
+@[expose] public section
+
+namespace Kildall
+
+/-- The state of a dataflow analysis on graph `g` is a mapping from nodes `n`
+    of `g` to elements of the abstract domain `L`. -/
+abbrev DFState (g : CFG) (L : Type) : Type := g.Node → L
+
+namespace DFState
+
+variable {L : Type} [SemilatticeSup L]
+
+/-- The empty dataflow result, a function mapping every node to `⊥`. -/
+def empty {g : CFG} [OrderBot L] : DFState g L := fun _ => ⊥
+
+/-- Update the value of `ρ` at node `n`, to new value `v`. -/
+def update {g : CFG} (ρ : DFState g L) (n : g.Node) (v : L) : DFState g L :=
+  letI := g.dEqNode
+  fun m => if m = n then v else ρ m
+
+/-- Updating `ρ` at `n` with a value bigger than `ρ n` yields a bigger `ρ` -/
+theorem lt_update {g : CFG} (ρ : DFState g L) (n : g.Node) (v : L) (hlt : ρ n < v) :
+    ρ < ρ.update n v := by
+  rw [Pi.lt_def]
+  refine ⟨fun m => ?_, n, ?_⟩ <;> grind [DFState.update]
+
+end DFState
+
+section Kildall
+
+variable {L : Type} [SemilatticeSup L] [DecidableEq L] [OrderBot L]
+variable {g : CFG}
+
+/-- If there's no ascending chains in `L`, there are no ascending chains in `DFState g L` either -/
+local instance {g : CFG} [WellFoundedGT L] : WellFoundedGT (DFState g L) :=
+  -- since Mathlib only defines LT wellfoundedness for functions, we need to do some flips
+  inferInstanceAs (WellFoundedLT (g.Node → Lᵒᵈ))
+
+/-- Wellfoundedness of state ordering based on WellFoundedGT. -/
+local instance {g : CFG} [WellFoundedGT L] : WellFoundedRelation (DFState g L) :=
+  ⟨(· > ·), IsWellFounded.wf⟩
+
+/-- Convenience type for a transfer function over nodes. -/
+abbrev NodeTransfer (g : CFG) (L : Type) := g.Node -> L -> L
+/-- Convenience type for a transfer function over edges. -/
+abbrev EdgeTransfer (g : CFG) (L : Type) := ∀ {src dst : g.Node}, g.Edge src dst -> L -> L
+
+/-- For a given CFG `g`, at node `n`, computes the join operation of all states incoming from
+    predecessor nodes through their relative edge transfers. Accounts for initialization at the
+    entry node. -/
+def joinPred {g : CFG} (eT : EdgeTransfer g L) (init : L) (ρ : DFState g L) (n : g.Node) : L :=
+  letI := g.dEqNode
+  (g.inEdges n).fold (· ⊔ ·)
+    (if n = g.entry then init else ⊥)
+    (fun ⟨n, e⟩ => eT e (ρ n))
+
+/-- Kildall's worklist algorithm, propagating updates to the worklist based on new information.
+    The termination proof uses wellfoundedness of · < · on `L`, i.e. the fact that the lattice
+    is of finite height. -/
+@[simp]
+def kildall [WellFoundedGT L] {g : CFG}
+    (nT : NodeTransfer g L) (eT : EdgeTransfer g L)
+    (init : L) (ρ : DFState g L := DFState.empty)
+    (wl : List (g.Node) := g.nodeList) : DFState g L :=
+  letI := g.orderNode
+  match wl with
+  | [] => ρ
+  | n :: rest =>
+      let newIn := joinPred eT init ρ n
+      let newOut := (ρ n) ⊔ (nT n newIn)
+      if _h : newOut = (ρ n) then
+        kildall nT eT init ρ rest
+      else
+        let ρ' := DFState.update ρ n newOut
+        let wl' := rest ++ (g.succOf n).sort
+        kildall nT eT init ρ' wl'
+termination_by (ρ, wl.length)
+decreasing_by
+  · exact Prod.Lex.right ρ (by simp)
+  · refine Prod.Lex.left _ _ ?_
+    apply DFState.lt_update
+    apply le_sup_left.lt_of_ne; grind
+
+end Kildall
+
+-- Our analysis lattice.
+variable {L : Type} [SemilatticeSup L] [WellFoundedGT L] [OrderBot L]
+
+/- ### Definitions -/
+
+/-- An analysis result `ρ` on `g` is a postfixpoint if, at every node of `g`, computing the
+    transfers of the incoming facts remains within the outgoing facts. -/
+def ForwardPostFixpoint
+    {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L)
+    (ρ : DFState g L) (wl : List (g.Node)) : Prop :=
+  ∀ n ∉ wl, nT n (joinPred eT init ρ n) ≤ ρ n
+
+/-- An analysis result `ρ` on `g` is a fixpoint if, at every node of `g`, the `ForwardPostFixpoint`
+    bound is tight. -/
+def ForwardFixpoint
+    {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L)
+    (ρ : DFState g L) (wl : List (g.Node)) : Prop :=
+  ∀ n ∉ wl, nT n (joinPred eT init ρ n) = ρ n
+
+/-- An analysis result `ρ` on `g` is a prefixpoint if every outgoing fact remains within the
+    result of transferring its incoming facts. -/
+def ForwardPreFixpoint {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L)
+    (ρ : DFState g L) : Prop :=
+  ∀ n, ρ n ≤ nT n (joinPred eT init ρ n)
+
+/- ### Helpers -/
+
+omit [WellFoundedGT L] in
+/-- Updating the abstract state at node `m` doesn't impact the incoming state at node `n` if `m` is
+    not a predecessor of `n`. -/
+lemma joinPred_neq_of_nonpred {g : CFG} (eT : EdgeTransfer g L) (init : L)
+    (ρ : DFState g L) (n m : g.Node) (v : L) (hm : n ∉ g.succOf m) :
+    joinPred eT init (ρ.update m v) n = joinPred eT init ρ n := by
+  simp only [joinPred]
+  apply Finset.fold_congr
+  intro e _
+  simp only [DFState.update]
+  split
+  case isFalse hneq => rfl
+  case isTrue heq =>
+    subst m
+    exfalso
+    apply hm
+    apply (@Finset.mem_image _ _ g.dEqNode).mpr
+    exact ⟨⟨n, e.2⟩, by simp [CFG.outEdges], rfl⟩
+
+omit [WellFoundedGT L] in
+/-- Incoming states are monotone when every edge transfer is monotone. -/
+lemma monotone_joinPred {g : CFG} (eT : EdgeTransfer g L) (init : L)
+    (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e)) :
+    Monotone (joinPred (g := g) eT init) := by
+  intro ρ₁ ρ₂ hle
+  apply Pi.le_def.2
+  intro n
+  simp only [joinPred]
+  suffices ∀ init₁ init₂, init₁ <= init₂ →
+    (g.inEdges n).fold (fun x y : L => x ⊔ y) init₁ (fun e => eT e.2 (ρ₁ e.1)) ≤
+      (g.inEdges n).fold (fun x y : L => x ⊔ y) init₂ (fun e => eT e.2 (ρ₂ e.1)) by
+    apply Std.IsPreorder.le_refl _ |> this _ _
+  induction g.inEdges n using Finset.cons_induction with
+  | empty => simp
+  | cons e s hnmem ih =>
+    intros i₁ i₂ hlei
+    rw [Finset.fold_cons hnmem, Finset.fold_cons hnmem]
+    exact sup_le_sup (heT e.2 (hle e.1)) (ih _ _ hlei)
+
+/-- The result of the worklist algorithm satisfies any invariant preserved through the
+    algorithm's run. Technique borrowed from @LaSpina25 -/
+lemma kildall_invariant [DecidableEq L]
+    {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L)
+    (init : L) (ρ : DFState g L) (wl : List (g.Node))
+    (P : DFState g L → List (g.Node) → Prop)
+    (hinit : P ρ wl)
+    (hstep_same : ∀ {ρ n rest}, P ρ (n :: rest) →
+      let newOut := ρ n ⊔ nT n (joinPred eT init ρ n)
+      newOut = ρ n →
+        P ρ rest)
+    (hstep_changed : ∀ {ρ n rest}, P ρ (n :: rest) →
+      let newOut := ρ n ⊔ nT n (joinPred eT init ρ n)
+      newOut ≠ ρ n →
+        P (ρ.update n newOut) (rest ++ (g.succOf n).sort)) :
+      P (kildall nT eT init ρ wl) [] := by
+  induction ρ, wl using kildall.induct nT eT init with
+  | case1 o => simpa
+  | case2 acc n rest nin nout heq ih =>
+      simp only [kildall, dite_eq_ite]
+      rw [if_pos heq]
+      exact ih (hstep_same hinit heq)
+  | case3 acc n r nin nout hnout acc' wl' ih =>
+      simp only [kildall, dite_eq_ite]
+      rw [if_neg hnout]
+      exact ih (hstep_changed hinit hnout)
+
+/- ### Theorems -/
+
+/-- The result of the worklist algorithm on appropriate intermediate state is a
+    `ForwardPostFixpoint`. -/
+theorem kildall_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG}
+    (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L) (ρ : DFState g L)
+    (wl : List (g.Node))
+    (hinv0 : ∀ m : g.Node, m ∉ wl → nT m (joinPred eT init ρ m) ≤ ρ m) :
+    let res := kildall nT eT init ρ wl
+    ForwardPostFixpoint nT eT init res [] := by
+  refine kildall_invariant nT eT init ρ wl (ForwardPostFixpoint nT eT init) ?_ ?_ ?_
+  · exact hinv0
+  · intro ρ n rest hfp newOut heq m hm
+    by_cases hmn : m = n
+    · subst m
+      exact le_sup_right.trans_eq heq
+    · exact hfp m (by simp_all)
+  · intro ρ n rest hfp newOut hnout m hm
+    have hsucc : m ∉ g.succOf n := fun hin =>
+      hm (List.mem_append_right _ ((g.succOf n).mem_sort (· ≤ ·) |>.mpr hin))
+    rw [joinPred_neq_of_nonpred eT init ρ m n newOut hsucc, DFState.update]
+    split -- m ?= n
+    case isTrue heq =>
+      grind [le_sup_right]
+    case isFalse hneq =>
+      apply hfp; grind
+
+/-- The result of the worklist algorithm on appropriate intermediate state is the least
+    `ForwardPostFixpoint`. -/
+theorem kildall_least_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG}
+    (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n))
+    (eT : EdgeTransfer g L)
+    (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e))
+    (init : L) (ρ σ : DFState g L) (wl : List (g.Node))
+    (hρ : ρ ≤ σ) (hσ : ForwardPostFixpoint nT eT init σ []) :
+    kildall nT eT init ρ wl ≤ σ := by
+  refine kildall_invariant nT eT init ρ wl
+    (fun ρ _ => ρ ≤ σ) hρ ?_ ?_
+  · exact fun hle _ => hle
+  · intro ρ n rest hle newOut hnout m
+    simp only [DFState.update]
+    split
+    case isTrue heq =>
+      subst m
+      apply sup_le (hle n)
+      refine (hnT n (monotone_joinPred eT init heT hle n)).trans ?_
+      apply hσ n (by simp)
+    case isFalse hneq => exact hle m
+
+/-- The worklist algorithm preserves forward pre-fixpoints when all transfers are monotone. -/
+lemma kildall_forwardPreFixpoint_of_init [DecidableEq L] {g : CFG}
+    (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n))
+    (eT : EdgeTransfer g L)
+    (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e))
+    (init : L) (ρ : DFState g L) (wl : List (g.Node))
+    (hinv0 : ForwardPreFixpoint nT eT init ρ) :
+    let res := kildall nT eT init ρ wl
+    ForwardPreFixpoint nT eT init res := by
+  refine kildall_invariant nT eT init ρ wl
+    (fun ρ _ => ForwardPreFixpoint nT eT init ρ) hinv0 ?_ ?_
+  · exact fun hfp _ => hfp
+  · intro ρ n rest hfp newOut hnout m
+    have hle : ρ ≤ ρ.update n newOut := by
+      intro k
+      simp only [DFState.update]
+      split <;> grind [le_refl, le_sup_left]
+    have htransfer : nT m (joinPred eT init ρ m) ≤
+        nT m (joinPred eT init (ρ.update n newOut) m) :=
+      hnT m (monotone_joinPred eT init heT hle m)
+    grind [DFState.update, sup_le, hfp m]
+
+/-- If the transfer functions are monotone, the result of the worklist algorithm on appropriate
+    intermediate state is a `ForwardFixpoint`. -/
+theorem kildall_forwardFixpoint_of_init [DecidableEq L] {g : CFG}
+    (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n))
+    (eT : EdgeTransfer g L)
+    (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e))
+    (init : L) (ρ : DFState g L) (wl : List (g.Node))
+    (hpost0 : ∀ m ∉ wl, nT m (joinPred eT init ρ m) ≤ ρ m)
+    (hpre0 : ForwardPreFixpoint nT eT init ρ) :
+    let res := kildall nT eT init ρ wl
+    ForwardFixpoint nT eT init res [] := by
+  intro res
+  have hpost :=
+    kildall_forwardPostFixpoint_of_init nT eT init ρ wl hpost0
+  have hpre :=
+    kildall_forwardPreFixpoint_of_init nT hnT eT heT init ρ wl hpre0
+  intro n hn
+  exact le_antisymm (hpost n hn) (hpre n)
+
+/-- Running Kildall's algorithm yields a postfixpoint of the forward dataflow constraints. -/
+theorem kildall_forwardPostFixpoint [DecidableEq L] (g : CFG)
+    (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L) :
+    let res := kildall (g := g) nT eT init
+    ForwardPostFixpoint (g := g) nT eT init res [] := by
+  apply kildall_forwardPostFixpoint_of_init nT eT init
+  -- `∀ m ∉ g.nodesOf, ...`
+  -- since every `m` is in `g.nodesOf` this is vacuously true
+  intro m hm
+  exact (hm (g.mem_nodeList m)).elim
+
+theorem kildall_least_forwardPostFixpoint [DecidableEq L] (g : CFG)
+    (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n))
+    (eT : EdgeTransfer g L)
+    (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e))
+    (init : L) (σ : DFState g L) (hfpf : ForwardPostFixpoint nT eT init σ []) :
+    kildall (g := g) nT eT init ≤ σ := by
+  apply kildall_least_forwardPostFixpoint_of_init nT hnT eT heT init DFState.empty σ g.nodeList
+    <;> simp [Pi.le_def, DFState.empty, hfpf]
+
+/-- If all transfer functions are monotone, running Kildall's algorithm yields a fixpoint of the
+     forward dataflow equations. -/
+theorem kildall_forwardFixpoint [DecidableEq L] (g : CFG)
+    (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n))
+    (eT : EdgeTransfer g L)
+    (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e))
+    (init : L) :
+    let res := kildall (g := g) nT eT init
+    ForwardFixpoint (g := g) nT eT init res [] := by
+  apply kildall_forwardFixpoint_of_init nT hnT eT heT init DFState.empty g.nodeList
+  case hpost0 => -- ≤
+    -- `∀ m ∉ g.nodesOf, ...`
+    -- since every `m` is in `g.nodesOf` this is vacuously true
+    intro m hm
+    exact (hm (g.mem_nodeList m)).elim
+  case hpre0 => -- ≥
+    -- `∀ m ∈ g.nodesOf, DFState.empty m ≤ ...`
+    -- since `DFState.empty` is `λ _. ⊥`, it's ≤ anything, thanks to `OrderBot`.
+    simp [ForwardPreFixpoint, DFState.empty]
+
+end Kildall
diff --git a/references.bib b/references.bib
index 6af9dafc4..b6b3dff36 100644
--- a/references.bib
+++ b/references.bib
@@ -509,3 +509,48 @@ @book{Papadimitriou94
   publisher={Addison-Wesley},
   address={Reading, Massachusetts}
 }
+
+@inproceedings{Kildall73,
+  author    = {Kildall, Gary A.},
+  title     = {A unified approach to global program optimization},
+  year      = {1973},
+  isbn      = {9781450373494},
+  publisher = {Association for Computing Machinery},
+  address   = {New York, NY, USA},
+  url       = {https://doi.org/10.1145/512927.512945},
+  doi       = {10.1145/512927.512945},
+  abstract  = {A technique is presented for global analysis of program structure in order to perform compile time optimization of object code generated for expressions. The global expression optimization presented includes constant propagation, common subexpression elimination, elimination of redundant register load operations, and live expression analysis. A general purpose program flow analysis algorithm is developed which depends upon the existence of an "optimizing function." The algorithm is defined formally using a directed graph model of program flow structure, and is shown to be correct. Several optimizing functions are defined which, when used in conjunction with the flow analysis algorithm, provide the various forms of code optimization. The flow analysis algorithm is sufficiently general that additional functions can easily be defined for other forms of global code optimization.},
+  booktitle = {Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
+  pages     = {194-206},
+  numpages  = {13},
+  location  = {Boston, Massachusetts},
+  series    = {POPL '73}
+}
+
+@book{Nielson99,
+  address   = {Berlin, Heidelberg},
+  title     = {Principles of Program Analysis},
+  rights    = {http://www.springer.com/tdm},
+  isbn      = {978-3-642-08474-4},
+  url       = {http://link.springer.com/10.1007/978-3-662-03811-6},
+  doi       = {10.1007/978-3-662-03811-6},
+  publisher = {Springer Berlin Heidelberg},
+  author    = {Nielson, Flemming and Nielson, Hanne Riis and Hankin, Chris},
+  year      = {1999},
+  language  = {en}
+}
+
+@inproceedings{LaSpina25,
+  title       = {{Formal Verification of WTO-based Dataflow Solvers}},
+  author      = {La Spina, Rom{\'e}o and Demange, Delphine and Blazy, Sandrine},
+  url         = {https://hal.science/hal-04851724},
+  booktitle   = {{Programming Languages and Systems}},
+  address     = {Hamilton, Canada},
+  pages       = {1-27},
+  year        = {2025},
+  month       = May,
+  keywords    = {compiler optimization ; verified compilation ; static analysis},
+  pdf         = {https://hal.science/hal-04851724v1/file/paper.pdf},
+  hal_id      = {hal-04851724},
+  hal_version = {v1}
+}