1: \begin{abstract}

2: We introduce a numerical framework to verify the finite step convergence of first-order methods for parametric convex quadratic optimization.

3: We formulate the verification problem as a mathematical optimization problem where we maximize a performance metric (\eg, fixed-point residual at the last iteration) subject to constraints representing proximal algorithm steps (\eg, linear system solutions, projections, or gradient steps). 

4: Our framework is highly modular because we encode a wide range of proximal algorithms as variations of two primitive steps: affine steps and element-wise maximum steps. 

5: Compared to standard convergence analysis and performance estimation techniques, we can explicitly quantify the effects of warm-starting by directly representing the sets where the initial iterates and parameters live.

6: We show that the verification problem is $\mathcal{NP}$-hard, and we construct strong semidefinite programming relaxations using various constraint tightening techniques.

7: Numerical examples in nonnegative least squares, network utility maximization, Lasso, and optimal control show a significant reduction in pessimism of our framework compared to standard worst-case convergence analysis techniques.

8: \end{abstract}

9: