The chapter discusses the use of dataflow analysis to approximate the behavior of functional programs without executing them. It introduces control flow analysis (CFA), which approximates the order of evaluation of expressions and commands. The analysis is applied to a labeled lambda calculus, where each expression has a unique label to track its behavior. The goal is to find functions \(\mathbf{C}\) and \(r\) that describe the possible values an expression or variable can evaluate to. The analysis generates constraints from the program and iteratively improves these constraints to reach a fixed point, providing a conservative approximation of the program's behavior. The chapter also introduces 1-CFA, an extension of CFA that considers the context in which expressions are called. This context is defined by the label of the calling function. The analysis uses pairs of labels and contexts to track the possible values of variables and expressions, ensuring that the analysis is more precise and context-sensitive. The chapter provides an example to illustrate how 1-CFA works and proves the soundness of the analysis, showing that it correctly describes the possible values and bindings of expressions and variables.The chapter discusses the use of dataflow analysis to approximate the behavior of functional programs without executing them. It introduces control flow analysis (CFA), which approximates the order of evaluation of expressions and commands. The analysis is applied to a labeled lambda calculus, where each expression has a unique label to track its behavior. The goal is to find functions \(\mathbf{C}\) and \(r\) that describe the possible values an expression or variable can evaluate to. The analysis generates constraints from the program and iteratively improves these constraints to reach a fixed point, providing a conservative approximation of the program's behavior. The chapter also introduces 1-CFA, an extension of CFA that considers the context in which expressions are called. This context is defined by the label of the calling function. The analysis uses pairs of labels and contexts to track the possible values of variables and expressions, ensuring that the analysis is more precise and context-sensitive. The chapter provides an example to illustrate how 1-CFA works and proves the soundness of the analysis, showing that it correctly describes the possible values and bindings of expressions and variables.