References — Chapter 14 · Dataflow Analysis & Abstract Interpretation

Every source this chapter cites, grouped by kind. Lessons cite entries inline as [KEY]; each entry says why and when to read it. Core reading marks the entries the chapter assumes you will open.

Foundational and research papers

• [AC76] Frances E. Allen and John Cocke. A Program Data Flow Analysis Procedure. Communications of the ACM 19(3), p. 137, 1976. doi:10.1145/360018.360025
  Why and when: Core reading. The interval-based elimination procedure of Lesson 14.5 (Algorithm 14.5.6) applied to the classic bit-vector problems; the paper that fixed the gen/kill vocabulary. Read after Lesson 14.5 §3.
  Cited in: overview, 02-monotone-frameworks, 03-classic-analyses, 04-iterative-solvers, 05-elimination-methods

• [All70] Frances E. Allen. Control Flow Analysis. SIGPLAN Notices 5(7), pp. 1-19 (Symposium on Compiler Optimization), 1970. doi:10.1145/390013.808479
  Why and when: Intervals and the derived sequence (Lesson 14.5 Definition 14.5.3), and the use-definition relationships that reaching definitions compute (Lesson 14.3). Read after Lesson 14.5 §2.
  Cited in: overview, 03-classic-analyses, 05-elimination-methods

• [BCC+03] Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A Static Analyzer for Large Safety-Critical Software. PLDI 2003, pp. 196-207, 2003. doi:10.1145/781131.781153
  Why and when: Astrée: abstract interpretation at industrial scale, widening with thresholds, octagon packs (Lesson 14.7 §6). Read for how the theory survives contact with 100 000-line programs.
  Cited in: 07-abstract-interpretation

• [BHG+08] Benoit Boissinot, Sebastian Hack, Daniel Grund, Benoît Dupont de Dinechin, and Fabrice Rastello. Fast Liveness Checking for SSA-Form Programs. CGO 2008, pp. 35-44, 2008. doi:10.1145/1356058.1356064
  Why and when: Answering "is v live at p?" without computing sets, from the dominator tree and loop structure (Lessons 14.3 and 14.6 §6). Useful before Ch 16's SSA destruction.
  Cited in: 03-classic-analyses, 06-sparse-analysis

• [Bou93] François Bourdoncle. Efficient chaotic iteration strategies with widenings. Formal Methods in Programming and Their Applications (FMPA), LNCS 735, pp. 128-141, 1993. doi:10.1007/BFb0039704
  Why and when: Weak topological orders: iterate strongly connected components recursively and widen only at component heads. The order behind Clang's WTODataflowWorklist (Lessons 14.4 and 14.7 §6).
  Cited in: overview, 04-iterative-solvers, 07-abstract-interpretation

• [BR86] François Bancilhon and Raghu Ramakrishnan. An Amateur's Introduction to Recursive Query Processing Strategies. SIGMOD 1986, pp. 16-52, 1986. doi:10.1145/16894.16859
  Why and when: Naive and semi-naive evaluation and their costs (Lesson 14.8, Algorithms 14.8.3 and 14.8.4); the algorithm of lab requirement L3. Read the semi-naive section before writing your evaluator.
  Cited in: overview, 08-datalog-and-ifds

• [BS09] Martin Bravenboer and Yannis Smaragdakis. Strictly Declarative Specification of Sophisticated Points-to Analyses. OOPSLA 2009, pp. 243-262, 2009. doi:10.1145/1640089.1640108
  Why and when: Core reading. Doop: a complete Java points-to analysis in Datalog, faster than the hand-written framework it was compared with (Lesson 14.8 §5). Read §2–3 for how an analysis becomes rules.
  Cited in: overview, 08-datalog-and-ifds

• [CC76] Patrick Cousot and Radhia Cousot. Static Determination of Dynamic Properties of Programs. Proceedings of the 2^nd International Symposium on Programming, Paris, Dunod, pp. 106-130, 1976.
  Why and when: The first interval analysis, with widening and narrowing: the domain of exercise E6 and of Lesson 14.7's worked example.
  Note: Conference proceedings without DOI; the authors' PDF is on Patrick Cousot's publication page.
  Cited in: overview, 07-abstract-interpretation

• [CC77] Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977, pp. 238-252, 1977. doi:10.1145/512950.512973
  Why and when: Core reading. The founding paper of abstract interpretation: collecting semantics, abstraction and concretization, widening and narrowing (Lesson 14.7, Definitions 14.7.1–14.7.9 and Theorem 14.7.10). Read after Lesson 14.7 §2.
  Cited in: overview, 01-lattices-and-fixed-points, 07-abstract-interpretation

• [CC79] Patrick Cousot and Radhia Cousot. Systematic Design of Program Analysis Frameworks. POPL 1979, pp. 269-282, 1979. doi:10.1145/567752.567778
  Why and when: Core reading. Galois connections as the design method, best transformers and the reduced product of domains (Lesson 14.7, Lemma 14.7.3 and §6). Read after Lesson 14.7 §4.
  Cited in: overview, 01-lattices-and-fixed-points, 02-monotone-frameworks, 07-abstract-interpretation

• [CC79b] Patrick Cousot and Radhia Cousot. Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics 82(1), pp. 43-57, 1979. doi:10.2140/pjm.1979.82.43
  Why and when: Fixed points as limits of (transfinite) iteration sequences: the constructive side of Theorem 14.1.14 (Kleene iteration). Optional mathematical background for Lesson 14.1 §4.
  Cited in: overview, 01-lattices-and-fixed-points

• [CC92] Patrick Cousot and Radhia Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation 2(4), pp. 511-547, 1992. doi:10.1093/logcom/2.4.511
  Why and when: Frameworks without a best abstraction (concretization only), and when widening is needed; the reference for Lesson 14.7 §6's first variant.
  Cited in: overview, 07-abstract-interpretation

• [CCF91] Jong-Deok Choi, Ron Cytron, and Jeanne Ferrante. Automatic Construction of Sparse Data Flow Evaluation Graphs. POPL 1991, pp. 55-66, 1991. doi:10.1145/99583.99594
  Why and when: Core reading. Sparse evaluation graphs (Lesson 14.6, Definition 14.6.8 and Algorithm 14.6.9): the per-problem generalization of SSA. Read §2–3 after Lesson 14.6 §2.
  Cited in: overview, 02-monotone-frameworks, 06-sparse-analysis

• [CFRWZ91] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM TOPLAS 13(4), pp. 451-490, 1991. doi:10.1145/115372.115320
  Why and when: SSA construction with iterated dominance frontiers; SSA is the sparse representation that makes Lesson 14.6 work. Ch 16 teaches it; here, read §1–2 for why phis sit where facts merge.
  Cited in: 03-classic-analyses, 06-sparse-analysis

• [CH78] Patrick Cousot and Nicolas Halbwachs. Automatic Discovery of Linear Restraints Among Variables of a Program. POPL 1978, pp. 84-96, 1978. doi:10.1145/512760.512770
  Why and when: The convex-polyhedra domain with its widening (Lesson 14.7, Definition 14.7.6); the invariant j = 2i of the islpy box is the kind of result it computes.
  Cited in: overview, 07-abstract-interpretation

• [Coc70] John Cocke. Global common subexpression elimination. SIGPLAN Notices 5(7), pp. 20-24 (Symposium on Compiler Optimization), 1970. doi:10.1145/390013.808480
  Why and when: Available expressions as a global bit-vector problem, the optimization behind Lesson 14.3's Algorithm 14.3.11. Short; read with Lesson 14.3 §1.
  Cited in: overview, 03-classic-analyses

• [EKL10] Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Journal of the ACM 57(6), Article 33, 2010. doi:10.1145/1857914.1857917
  Why and when: Newton's method instead of Kleene iteration on semiring equation systems; further reading after Lesson 14.5 §6 for the algebraic view of interprocedural analysis.
  Cited in: 05-elimination-methods

• [Gra89] Philippe Granger. Static Analysis of Arithmetical Congruences. International Journal of Computer Mathematics 30(3-4), pp. 165-190, 1989. doi:10.1080/00207168908803778
  Why and when: The congruence domain aZ + b (Lesson 14.7, Definition 14.7.5); LLVM's KnownBits is its power-of-two special case.
  Cited in: overview, 07-abstract-interpretation

• [GW76] Susan L. Graham and Mark Wegman. A Fast and Usually Linear Algorithm for Global Flow Analysis. Journal of the ACM 23(1), pp. 172-202, 1976. doi:10.1145/321921.321939
  Why and when: An O(e log e) elimination algorithm for a broad class of frameworks on reducible graphs; the variant listed in Lesson 14.5 §6.
  Cited in: overview, 05-elimination-methods

• [HU75] Matthew S. Hecht and Jeffrey D. Ullman. A Simple Algorithm for Global Data Flow Analysis Problems. SIAM Journal on Computing 4(4), pp. 519-532, 1975. doi:10.1137/0204044
  Why and when: Round-robin iteration in reverse postorder and its pass bound for reducible graphs, before Kam and Ullman's general version; read with Lesson 14.4 §2.
  Cited in: overview, 04-iterative-solvers

• [JSS16] Herbert Jordan, Bernhard Scholz, and Pavle Subotić. Soufflé: On Synthesis of Program Analyzers. CAV 2016, LNCS 9780, pp. 422-430, 2016. doi:10.1007/978-3-319-41540-6_23
  Why and when: Core reading. Compiling Datalog to parallel C++ with specialized indexes: why declarative analyses can be fast (Lesson 14.8's Soufflé boxes). A short tool paper; read it all.
  Cited in: overview, 08-datalog-and-ifds

• [KD94] Uday P. Khedker and Dhananjay M. Dhamdhere. A Generalized Theory of Bit Vector Data Flow Analysis. ACM TOPLAS 16(5), pp. 1472-1511, 1994. doi:10.1145/186025.186043
  Why and when: Bidirectional bit-vector frameworks and their iteration complexity (Lesson 14.2 §6). Read if the unidirectional theory of Lesson 14.4 leaves you wondering what PRE's equations cost.
  Cited in: overview, 02-monotone-frameworks

• [Kil73] Gary A. Kildall. A unified approach to global program optimization. POPL 1973, 194–206, 1973. doi:10.1145/512927.512945
  Why and when: Core reading. The origin of iterative dataflow analysis: facts in a (meet) semilattice, a function per node, a worklist of nodes until nothing changes, correctness for distributive functions. Read it after Lesson 14.2 §2; constant propagation is its running example.
  Cited in: overview, 01-lattices-and-fixed-points, 02-monotone-frameworks, 03-classic-analyses, 04-iterative-solvers, 07-abstract-interpretation

• [KRS92] Jens Knoop, Oliver Rüthing, and Bernhard Steffen. Lazy Code Motion. PLDI 1992, pp. 224-234, 1992. doi:10.1145/143095.143136
  Why and when: PRE decomposed into unidirectional bit-vector problems (down-safety = anticipability, earliest, latest); the modern form of Lesson 14.3's very busy expressions. Ch 17 builds on it.
  Cited in: 03-classic-analyses

• [KU76] John B. Kam and Jeffrey D. Ullman. Global Data Flow Analysis and Iterative Algorithms. Journal of the ACM 23(1), pp. 158-171, 1976. doi:10.1145/321921.321938
  Why and when: Core reading. Rapid frameworks and the d(G) + 2 pass bound for round-robin iteration in reverse postorder (Theorem 14.4.6). Read §3–4 after Lesson 14.4 §2; the definition of loop connectedness is theirs.
  Cited in: overview, 01-lattices-and-fixed-points, 02-monotone-frameworks, 04-iterative-solvers, 05-elimination-methods

• [KU77] John B. Kam and Jeffrey D. Ullman. Monotone Data Flow Analysis Frameworks. Acta Informatica 7(3), pp. 305-317, 1977. doi:10.1007/BF00290339
  Why and when: Core reading. Monotone (not only distributive) frameworks: the MFP solution, its soundness with respect to MOP, equality under distributivity and the undecidability of MOP (Theorems 14.2.12–14.2.14). Read after Lesson 14.2; mind their downward orientation (Definition 14.2.3).
  Cited in: overview, 01-lattices-and-fixed-points, 02-monotone-frameworks

• [Min06] Antoine Miné. The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19(1), pp. 31-100, 2006. doi:10.1007/s10990-006-8609-1
  Why and when: Core reading. Octagons, difference-bound matrices, strong closure (Algorithm 14.7.7), widening, and their use in Astrée. Read the closure and widening sections after Lesson 14.7 §2.
  Cited in: overview, 07-abstract-interpretation

• [MR05] Laurent Mauborgne and Xavier Rival. Trace Partitioning in Abstract Interpretation Based Static Analyzers. ESOP 2005, LNCS 3444, pp. 5-20, 2005. doi:10.1007/978-3-540-31987-0_2
  Why and when: Keeping some paths apart instead of joining them: a controlled step from MFP towards MOP (Lesson 14.2 §6).
  Cited in: 02-monotone-frameworks

• [MR79] Etienne Morel and Claude Renvoise. Global optimization by suppression of partial redundancies. Communications of the ACM 22(2), pp. 96-103, 1979. doi:10.1145/359060.359069
  Why and when: Partial-redundancy elimination: availability and anticipability (very busy expressions) combined in a bidirectional bit-vector system. Read after Lesson 14.3 §6; Ch 17 treats PRE in full.
  Cited in: overview, 02-monotone-frameworks, 03-classic-analyses

• [RHS95] Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise Interprocedural Dataflow Analysis via Graph Reachability. POPL 1995, pp. 49-61, 1995. doi:10.1145/199448.199462
  Why and when: Core reading. IFDS: exploded supergraphs, realizable paths and the tabulation algorithm (Lesson 14.8, Definitions 14.8.6–14.8.7, Algorithm 14.8.8, Theorem 14.8.9). Read §2–4.
  Cited in: overview, 02-monotone-frameworks, 08-datalog-and-ifds

• [Sha80] Micha Sharir. Structural analysis: A new approach to flow analysis in optimizing compilers. Computer Languages 5(3-4), pp. 141-153, 1980. doi:10.1016/0096-0551(80)90007-7
  Why and when: The origin of structural analysis (Lesson 14.5, Algorithm 14.5.9): region schemas, the control tree, summaries per schema.
  Cited in: overview, 05-elimination-methods

• [SRH96] Mooly Sagiv, Thomas Reps, and Susan Horwitz. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. Theoretical Computer Science 167(1-2), pp. 131-170, 1996. doi:10.1016/0304-3975(96)00072-2
  Why and when: IDE: environment transformers with micro-functions on exploded edges, linear constant propagation (Lesson 14.8, Definition 14.8.10). Read after RHS95.
  Cited in: overview, 02-monotone-frameworks, 03-classic-analyses, 08-datalog-and-ifds

• [Tar55] Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), pp. 285-309, 1955. doi:10.2140/pjm.1955.5.285
  Why and when: Theorem 1 is the Knaster–Tarski theorem of Lesson 14.1 (Theorem 14.1.12), including the fact that the fixed points form a complete lattice. Two pages; read §1 only.
  Cited in: overview, 01-lattices-and-fixed-points

• [Tar81a] Robert Endre Tarjan. A Unified Approach to Path Problems. Journal of the ACM 28(3), pp. 577-593, 1981. doi:10.1145/322261.322272
  Why and when: Core reading. Path expressions and their interpretation in an algebra (Lesson 14.5, Definition 14.5.10 and Theorem 14.5.12): one framework for shortest paths, reachability and dataflow.
  Cited in: overview, 05-elimination-methods

• [Tar81b] Robert Endre Tarjan. Fast Algorithms for Solving Path Problems. Journal of the ACM 28(3), pp. 594-614, 1981. doi:10.1145/322261.322273
  Why and when: Computing path expressions in O(e α(e, n)) on reducible graphs through the dominator tree; the best elimination bound quoted in Lesson 14.5 §5.
  Cited in: overview, 05-elimination-methods

• [Ull73] Jeffrey D. Ullman. Fast algorithms for the elimination of common subexpressions. Acta Informatica 2(3), pp. 191-213, 1973. doi:10.1007/BF00289078
  Why and when: An O(e log e) elimination algorithm for available expressions on reducible graphs; the historical context for Lessons 14.3 and 14.5.
  Cited in: overview, 02-monotone-frameworks, 03-classic-analyses, 06-sparse-analysis

• [WL04] John Whaley and Monica S. Lam. Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams. PLDI 2004, pp. 131-144, 2004. doi:10.1145/996841.996859
  Why and when: bddbddb: Datalog over BDDs made context-sensitive points-to analysis practical (Lesson 14.8 §1 and §6).
  Cited in: overview, 08-datalog-and-ifds

• [WZ91] Mark N. Wegman and F. Kenneth Zadeck. Constant Propagation with Conditional Branches. ACM TOPLAS 13(2), pp. 181-210, 1991. doi:10.1145/103135.103136
  Why and when: Core reading. Sparse conditional constant propagation (Algorithm 14.6.6): values and executable edges solved together. GCC's tree-ssa-ccp.cc cites it in its header. Read §3–4 after Lesson 14.6.
  Cited in: overview, 03-classic-analyses, 06-sparse-analysis

Textbooks and monographs

• [AHV95] Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison-Wesley, 1995. Read: Part D: Ch. 12 (Datalog), Ch. 13 (Evaluation of Datalog), Ch. 15 (Negation in Datalog).
  Why and when: The textbook semantics of Datalog: least models, the immediate-consequence operator, semi-naive evaluation and stratified negation (Lesson 14.8, Definition 14.8.2).
  Cited in: overview, 08-datalog-and-ifds

• [Dragon2] Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools, 2^nd ed.. Addison-Wesley, 2006. Read: Ch. 9: §9.2 (introduction to data-flow analysis: reaching definitions, live variables, available expressions), §9.3 (foundations: semilattices, monotone frameworks, MOP/MFP), §9.4 (constant propagation), §9.6 (loops in flow graphs: depth and the speed of iterative algorithms), §9.7 (region-based analysis).
  Why and when: Core reading. The standard textbook treatment of Lessons 14.2–14.3 and of region-based (elimination) analysis; its §9.3 proofs are a good second reading after this chapter's.
  Cited in: 03-classic-analyses, 04-iterative-solvers, 05-elimination-methods

• [EaC3] Keith D. Cooper and Linda Torczon. Engineering a Compiler, 3^rd ed.. Morgan Kaufmann, 2022. Read: Ch. 9 (Data-Flow Analysis): §9.2 (iterative data-flow analysis: liveness, round-robin, RPO), §9.3 (SSA form).
  Why and when: The most practical account of iterative solvers and orders; read §9.2 alongside Lesson 14.4.
  Cited in: 03-classic-analyses

• [Muchnick] Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997. Read: Ch. 7 (Control-Flow Analysis: §7.6 interval analysis and control trees, §7.7 structural analysis), Ch. 8 (Data-Flow Analysis: iterative, lattices of flow functions, control-tree-based methods).
  Why and when: Full pseudo-code for interval and structural analysis (Lesson 14.5) and for flow-function lattices (Definition 14.5.1).
  Cited in: 05-elimination-methods

• [NNH] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer, 1999. Read: Ch. 2 (Data Flow Analysis: the four classics, monotone frameworks, MFP and MOP), Ch. 4 (Abstract Interpretation: widening, narrowing, Galois connections), Ch. 6 (Algorithms: worklists, reverse postorder, strong components), Appendix A (partially ordered sets and fixed points).
  Why and when: Core reading. The rigorous reference for Lessons 14.1, 14.2, 14.4 and 14.7; its Chapter 6 covers the solver orders of Lesson 14.4 in more depth than any compiler textbook.
  Cited in: 01-lattices-and-fixed-points, 04-iterative-solvers, 07-abstract-interpretation

• [SPA] Anders Møller and Michael I. Schwartzbach. Static Program Analysis. Aarhus University (online lecture notes), 2024. Read: Ch. 4 (Lattice Theory), Ch. 5 (Dataflow Analysis with Monotone Frameworks), Ch. 6 (Widening), Ch. 9 (Distributive Interprocedural Analysis: IFDS), Ch. 12 (Abstract Interpretation) — chapter numbers of the 2024 edition. link
  Why and when: Free, concise and precise; the best first reading for Lessons 14.1, 14.2 and 14.7, with the TIP teaching language (github.com/cs-au-dk/TIP) as a companion implementation.
  Note: Unverified: chapter numbers follow the 2024 edition's table of contents as recalled by the author and reviewer; cs.au.dk was unreachable from the course container, so check them against the current PDF (the notes are revised yearly and chapters get renumbered).
  Cited in: overview

• [SSAB] Fabrice Rastello and Florent Bouchez Tichadou. SSA-based Compiler Design. Springer, 2022. Read: Part II (Analysis): Ch. 8 (Propagating Information Using SSA), Ch. 9 (Liveness). doi:10.1007/978-3-030-80515-9
  Why and when: Sparse propagation and SSA liveness (Lessons 14.3 and 14.6, Definition 14.3.9 and Algorithm 14.6.4). Read Ch. 9 before the lab's L1.
  Cited in: 03-classic-analyses, 06-sparse-analysis

Surveys and tutorials

• [Ken81] Ken Kennedy. A survey of data flow analysis techniques. In S. S. Muchnick and N. D. Jones (eds.), Program Flow Analysis: Theory and Applications, Prentice-Hall, pp. 5-54, 1981.
  Why and when: The survey of the pre-SSA era: iterative, interval and elimination methods, def-use chains and the classic problems side by side. Read after Lessons 14.3–14.5 for the historical map.
  Note: A book chapter; no DOI. Found in university libraries.
  Cited in: 06-sparse-analysis

• [RP86] Barbara G. Ryder and Marvin C. Paull. Elimination Algorithms for Data Flow Analysis. ACM Computing Surveys 18(3), pp. 277-316, 1986. doi:10.1145/27632.27649
  Why and when: The comparative survey of Allen–Cocke, Hecht–Ullman, Graham–Wegman and Tarjan elimination methods with complexity tables; read after Lesson 14.5 to see all of them side by side.
  Cited in: overview, 05-elimination-methods

Theses and technical reports

• [Ana99] C. Scott Ananian. The Static Single Information Form. Master's thesis, Massachusetts Institute of Technology (MIT-LCS-TR-801), 1999.
  Why and when: SSI: sigma-functions at branches so that branch-refined facts become sparse too (Lesson 14.6 §6), the idea behind LLVM's PredicateInfo.
  Note: MIT technical report; no DOI.
  Cited in: 06-sparse-analysis

• [BBD+11] Florian Brandner, Benoit Boissinot, Alain Darte, Benoît Dupont de Dinechin, and Fabrice Rastello. Computing Liveness Sets for SSA-Form Programs. INRIA Research Report RR-7503, 2011. link
  Why and when: Path exploration versus iterative liveness on SSA, with measurements; the algorithm of the lab's sparse liveness (Algorithm 14.6.4). Read §2–3 before starting lab requirement L1.
  Cited in: overview, 03-classic-analyses, 06-sparse-analysis

• [CHK04] Keith D. Cooper, Timothy J. Harvey, and Ken Kennedy. Iterative Data-flow Analysis, Revisited. Rice University, Department of Computer Science, technical report TR04-432 (March 2004), 2004. link
  Why and when: Theory and measurements of the iterative algorithm: the role of reducibility in the Kam–Ullman bound, and experiments showing that round-robin and worklist variants behave very differently (a careful worklist wins; implementation mistakes reverse that). Read after Lesson 14.4; cited in Lesson 14.5 for why production compilers iterate. It does not benchmark elimination methods.
  Note: Report number and date from the Rice repository record (handle 1911/96324); the repository was not reachable from the review container, so the number was checked via its search-index entry only.
  Cited in: overview, 05-elimination-methods

Source code (pinned versions)

• [CLANG-DFA] Clang's dataflow framework (typed lattice + transfer functions) — clang/include/clang/Analysis/FlowSensitive/DataflowAnalysis.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: DataflowAnalysis, runDataflowAnalysis.
  Why and when: A modern Kildall framework in C++ (Lessons 14.1 and 14.2); the unchecked-optional-access check is built on it.
  Cited in: 01-lattices-and-fixed-points, 02-monotone-frameworks

• [CLANG-DFW] Clang's worklists ordered by RPO or by a weak topological order — clang/include/clang/Analysis/FlowSensitive/DataflowWorklist.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: DataflowWorklistBase, ReversePostOrderCompare, ForwardDataflowWorklist, BackwardDataflowWorklist, WTODataflowWorklist.
  Why and when: Algorithm 14.4.2's priority discipline in 100 lines (Lesson 14.4).
  Cited in: 04-iterative-solvers

• [CLANG-LV] Live variables on Clang's CFG — clang/lib/Analysis/LiveVariables.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: LiveVariables::computeLiveness.
  Why and when: A backward worklist liveness used by the dead-store checker (Lesson 14.3's analyzer box).
  Cited in: 03-classic-analyses

• [CLANG-SA] The static analyzer's loop widening (see also ExprEngine.cpp and RangeConstraintManager.cpp) — clang/lib/StaticAnalyzer/Core/LoopWidening.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: getWidenedLoopState.
  Why and when: Widening in a path-sensitive analyzer (Lesson 14.7's last box); ExprEngine.cpp explores paths and RangeConstraintManager.cpp keeps each symbol's range set.
  Cited in: 02-monotone-frameworks, 07-abstract-interpretation

• [CLANG-UNINIT] The analysis behind -Wuninitialized and -Wsometimes-uninitialized — clang/lib/Analysis/UninitializedValues.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: runUninitializedVariablesAnalysis, CFGBlockValues, TransferFunctions.
  Why and when: Definite initialization as a forward worklist over packed bit vectors (Lessons 14.3 and 14.4).
  Cited in: 03-classic-analyses, 04-iterative-solvers

• [GCC-CCP] GCC's conditional constant propagation on SSA — gcc/tree-ssa-ccp.cc in gcc-mirror/gcc at releases/gcc-15. Symbols: ccp_lattice_t.
  Why and when: Wegman–Zadeck CCP with a four-level lattice; its header comment is a good summary of Algorithm 14.6.6 (Lessons 14.3 and 14.6).
  Cited in: 01-lattices-and-fixed-points, 02-monotone-frameworks, 03-classic-analyses, 06-sparse-analysis

• [GCC-DF] GCC's RTL dataflow framework (problems in gcc/df-problems.cc) — gcc/df-core.cc in gcc-mirror/gcc at releases/gcc-15. Symbols: df_analyze, df_analyze_problem, df_worklist_dataflow, df_worklist_dataflow_doublequeue.
  Why and when: A production worklist solver over bitmaps with the live-register and reaching-definitions problems (Lessons 14.2–14.4); the dump boxes show its visit counts.
  Cited in: 02-monotone-frameworks, 03-classic-analyses, 04-iterative-solvers

• [GCC-RANGER] GCC's on-demand range analysis (Ranger) — gcc/gimple-range.cc in gcc-mirror/gcc at releases/gcc-15. Symbols: gimple_ranger::range_of_stmt.
  Why and when: Intervals (multi-ranges) on demand, the engine behind VRP (Lesson 14.7 §7).
  Cited in: 07-abstract-interpretation

• [GCC-UNINIT] GCC's -Wuninitialized and -Wmaybe-uninitialized — gcc/tree-ssa-uninit.cc in gcc-mirror/gcc at releases/gcc-15. Symbols: warn_uninitialized_vars, execute_late_warn_uninitialized.
  Why and when: Uninitialized-use warnings on optimized SSA with predicate analysis (Lesson 14.3).
  Cited in: 03-classic-analyses

• [LLVM-CR] Wrapped intervals of APInts — llvm/include/llvm/IR/ConstantRange.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: ConstantRange::unionWith, ConstantRange::addWithNoWrap.
  Why and when: The interval domain LLVM uses, including no-wrap-aware arithmetic (Lesson 14.7 §7 and the nsw rule of exercise E6).
  Cited in: 01-lattices-and-fixed-points, 07-abstract-interpretation

• [LLVM-DB] Demanded bits, a backward analysis along use-def chains — llvm/lib/Analysis/DemandedBits.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: DemandedBits::performAnalysis.
  Why and when: Liveness at bit granularity, computed sparsely over instructions (Lesson 14.6's first box).
  Cited in: 06-sparse-analysis

• [LLVM-EARLYCSE] Dominator-tree CSE with scoped tables of available expressions — llvm/lib/Transforms/Scalar/EarlyCSE.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: EarlyCSE.
  Why and when: Available expressions without iteration, thanks to SSA (Lesson 14.3's EarlyCSE box).
  Cited in: 03-classic-analyses

• [LLVM-GVNHOIST] Code hoisting based on ANTIC (very busy) points — llvm/lib/Transforms/Scalar/GVNHoist.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: GVNHoist.
  Why and when: Very busy expressions put to work (Lesson 14.3's GVNHoist box); read the file comment.
  Cited in: 03-classic-analyses

• [LLVM-IC] Folding operations through phis, per incoming edge — llvm/lib/Transforms/InstCombine/InstructionCombining.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: InstCombinerImpl::foldBinopWithPhiOperands, InstCombinerImpl::foldOpIntoPhi.
  Why and when: How -O2 recovers the MOP answer of Lesson 14.2's example by evaluating per path after the fact.
  Cited in: 02-monotone-frameworks

• [LLVM-KB] Known-zero/known-one bit abstraction — llvm/include/llvm/Support/KnownBits.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: KnownBits.
  Why and when: A bit-level domain; its low bits are the power-of-two congruences of Definition 14.7.5.
  Cited in: 07-abstract-interpretation

• [LLVM-LI] Natural loops (and llvm/include/llvm/Analysis/CycleAnalysis.h for cycles) — llvm/include/llvm/Analysis/LoopInfo.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: LoopInfo.
  Why and when: The loop nesting forest that intervals approximate (Lesson 14.5); Ch 15 builds it.
  Cited in: 05-elimination-methods

• [LLVM-LV] SSA liveness of virtual registers on Machine IR — llvm/lib/CodeGen/LiveVariables.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: LiveVariables::analyze, LiveVariables::MarkVirtRegAliveInBlock, LiveVariables::HandleVirtRegUse.
  Why and when: The path-exploration liveness of Algorithm 14.6.4, producing the kill flags register allocation needs (Lessons 14.3 and 14.6).
  Cited in: 03-classic-analyses, 06-sparse-analysis

• [LLVM-LVI] On-demand interval analysis per (value, block) — llvm/lib/Analysis/LazyValueInfo.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: LazyValueInfoImpl::solve, LazyValueInfoImpl::solveBlockValue.
  Why and when: A demand-driven interval analysis with branch refinement on edges, the closest LLVM relative of exercise E6 (Lessons 14.1 and 14.7).
  Cited in: 07-abstract-interpretation

• [LLVM-MSSA] MemorySSA, a sparse evaluation graph for memory — llvm/lib/Analysis/MemorySSA.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: MemorySSA::buildMemorySSA, MemorySSA::placePHINodes.
  Why and when: MemoryPhis at iterated dominance frontiers and uses linked to dominating defs (Lesson 14.6, Definition 14.6.8).
  Cited in: 06-sparse-analysis

• [LLVM-RDA] Reaching definitions of physical registers after register allocation — llvm/lib/CodeGen/ReachingDefAnalysis.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: ReachingDefInfo::run, ReachingDefInfo::processBasicBlock, ReachingDefInfo::reprocessBasicBlock.
  Why and when: Reaching definitions with LoopTraversal's two-pass order (Lessons 14.3 and 14.4 §6).
  Cited in: 03-classic-analyses, 04-iterative-solvers

• [LLVM-RI] Single-entry single-exit regions — llvm/lib/Analysis/RegionInfo.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: RegionInfo.
  Why and when: The region tree that structural analysis would summarize (Lesson 14.5's RegionInfo box).
  Cited in: 05-elimination-methods

• [LLVM-SCCP] LLVM's sparse conditional constant (and range) propagation solver — llvm/lib/Transforms/Utils/SCCPSolver.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: SCCPInstVisitor::solve, SCCPInstVisitor::markEdgeExecutable, MaxNumRangeExtensions.
  Why and when: Wegman–Zadeck SCCP over ValueLatticeElement, with executable edges and range widening (Lessons 14.1, 14.6 and 14.7).
  Cited in: 01-lattices-and-fixed-points, 03-classic-analyses, 04-iterative-solvers, 06-sparse-analysis, 07-abstract-interpretation

• [LLVM-SCEV] Scalar evolution's closed-form loop recurrences — llvm/lib/Analysis/ScalarEvolution.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: ScalarEvolution::createAddRecFromPHI.
  Why and when: Loops summarized in closed form, the production descendant of elimination methods (Lesson 14.5).
  Cited in: 05-elimination-methods

• [LLVM-SL] Stack-slot liveness by round-robin iteration over bit vectors — llvm/lib/Analysis/StackLifetime.cpp in llvm/llvm-project at llvmorg-23.1.2. Symbols: StackLifetime::calculateLocalLiveness.
  Why and when: Algorithm 14.4.1 in production, with a TODO to switch to a worklist (Lesson 14.4).
  Cited in: 04-iterative-solvers

• [LLVM-SPARSE] LLVM's generic sparse propagation solver (Kildall-style framework as a template) — llvm/include/llvm/Analysis/SparsePropagation.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: AbstractLatticeFunction, SparseSolver, SparseSolver::Solve.
  Why and when: The framework interface (lattice values, MergeValues, ComputeInstructionState) and the solver (Lessons 14.2 and 14.6); its client is CalledValuePropagation.cpp.
  Cited in: 02-monotone-frameworks, 06-sparse-analysis

• [LLVM-VL] The value lattice shared by SCCP and LazyValueInfo — llvm/include/llvm/Analysis/ValueLattice.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: ValueLatticeElement, ValueLatticeElement::mergeIn, ValueLatticeElement::MergeOptions.
  Why and when: unknown/undef/constant/notconstant/constantrange/overdefined, the join (mergeIn) and the simple widening by extension count (Lessons 14.1 and 14.7).
  Cited in: 01-lattices-and-fixed-points, 07-abstract-interpretation

• [MLIR-DF] MLIR's dataflow solver (with DataFlow/SparseAnalysis.h, IntegerRangeAnalysis.h, LivenessAnalysis.h) — mlir/include/mlir/Analysis/DataFlowFramework.h in llvm/llvm-project at llvmorg-23.1.2. Symbols: DataFlowSolver, DataFlowAnalysis.
  Why and when: One solver running dense and sparse analyses together; its sparse analyses are Algorithm 14.6.2 over MLIR values (Lessons 14.1, 14.2 and 14.6).
  Cited in: 01-lattices-and-fixed-points, 02-monotone-frameworks, 03-classic-analyses, 06-sparse-analysis, 07-abstract-interpretation

• [RUSTC-DF] rustc's MIR dataflow framework (lattices in framework/lattice.rs, analyses in impls/) — compiler/rustc_mir_dataflow/src/framework/mod.rs in rust-lang/rust at 1.90.0. Symbols: Analysis, Analysis::iterate_to_fixpoint.
  Why and when: A trait-based monotone framework with an RPO-seeded work queue; MaybeLiveLocals and MaybeUninitializedPlaces feed the borrow checker (Lessons 14.1–14.4).
  Cited in: 01-lattices-and-fixed-points, 02-monotone-frameworks, 03-classic-analyses, 04-iterative-solvers

Official documentation and specifications

• [CLANG-DFDOC] Data flow analysis: an informal introduction (Clang documentation). LLVM 23.1.2. link
  Why and when: Clang's own tutorial for its dataflow framework: lattices, joins, fixpoint iteration and the termination argument, with CFG pictures. Read after Lesson 14.1 as a friendly second view.
  Cited in: 01-lattices-and-fixed-points

• [DOOP-DOC] Doop: Datalog 101 and Doop 101. link
  Why and when: Doop's introduction to Datalog and its evaluation to a fixed point, and (docs/doop-101.md) how its points-to results are queried. Read after Lesson 14.8 §2.
  Cited in: 08-datalog-and-ifds

• [JLS] The Java Language Specification, Java SE 21 Edition, Chapter 16: Definite Assignment. Java SE 21. link
  Why and when: Definite initialization as a language rule, specified construct by construct (Lesson 14.3, Definition 14.3.19 and §6).
  Cited in: overview, 03-classic-analyses

• [MLIR-DFDOC] Writing DataFlow Analyses in MLIR. LLVM 23.1.2. link
  Why and when: How MLIR's DataFlowSolver runs several sparse and dense analyses together; read after Lesson 14.6 to see Algorithm 14.6.2 as a reusable framework.

• [SOUFFLE-DOC] Soufflé: project README and language documentation. Soufflé 2.5. link
  Why and when: Installation (release packages) and the language; the Datalog dialect of Lesson 14.8's boxes. Read before running the Soufflé boxes.
  Cited in: 08-datalog-and-ifds