\begin{algorithm}
        \caption{Tabulation Algorithm}
        \begin{algorithmic}
        \INPUT Exploded supergraph $G^{\sharp}$ of a program.
        \OUTPUT Solution to the realizable-path reachability problem.
        \STATE \textbf{declare} PathEdge, WorkList, SummaryEdge: \textbf{global} edge set
        \STATE Let $(N^{\sharp}, E^{\sharp}) = G^{\sharp}$
        \STATE PathEdge := $\{(s_{main}, 0) \to (s_{main}, 0)\}$
        \STATE WorkList := $\{(s_{main}, 0) \to (s_{main}, 0)\}$
        \STATE SummaryEdge := $\emptyset$
        \STATE \CALL{ForwardTabulateSLRPs}{}
        \FOR{\textbf{each} $n \in N^{*}$}
            \STATE $X_n$ := $\{d_2 \in D | \exists d_1 \in (D \cup \{0\})$ such that $(s_{procOf(n)}, d_1) \to (n, d_2) \in PathEdge\}$
            \STATE \COMMENT{$procOf$ maps a node to the name of its enclosing procedure.}
        \ENDFOR
        \STATE
        \PROCEDURE{Propagate}{$e$}
            \IF{$e \notin$ PathEdge}
                \STATE Insert $e$ into PathEdge.
                \STATE Insert $e$ into WorkList.
            \ENDIF
        \ENDPROCEDURE
        \STATE
        \PROCEDURE{ForwardTabulateSLRPs}{}
            \WHILE{WorkList $\ne \emptyset$}
                \STATE Select and remove an edge $(s_p, d_1) \to (n, d_2)$ from WorkList.
                \IF{$n \in Call_p$}
                    \FOR{\textbf{each} $d_3$ such that $(n, d_2) \to (s_{calledProc(n)}, d_3) \in E^{\sharp}$}
                        \STATE \CALL{Propagate}{$(s_{calledProc(n)}, d_3) \to (s_{calledProc(n)}, d_3)$}
                        \STATE \COMMENT{$calledProc$ maps a call node to the name of the called procedure.}
                    \ENDFOR
                    \FOR{\textbf{each} $d_3$ such that $(n, d_2) \to (returnSite(n), d_3) \in (E^{\sharp} \cup SummaryEdge)$}
                        \STATE \CALL{Propagate}{$(s_p, d_1) \to (returnSite(n), d_3)$}
                        \STATE \COMMENT{$returnSite$ maps a call node to its corresponding return-site node.}
                    \ENDFOR
                \ELIF{$n = e_p$}
                    \FOR{\textbf{each} $c \in callers(p)$}
                        \STATE \COMMENT{$callers$ maps a procedure name to the set of call nodes that represents calls to that procedure.}
                        \FOR{\textbf{each} $d_4, d_5$ such that $(c, d_4)\to (d_p, d_1) \in E^{\sharp}$ \AND $(e_p, d_2)\to(returnSite(c), d_5)\in E^{\sharp}$}
                            \IF{$(c, d_4) \to (returnSite(c), d_5) \notin$ SummaryEdge}
                                \STATE Insert $(c, d_4) \to (returnSite(c), d_5)$ into SummaryEdge.
                                \FOR{\textbf{each} $d_3$ such that $(s_{procOf(c)}, d_3) \to (c, d_4) \in$ PathEdge}
                                    \STATE \CALL{Propagate}{$(s_{procOf(c)}, d_3) \to (returnSite(c), d_5)$}
                                \ENDFOR
                            \ENDIF
                        \ENDFOR
                    \ENDFOR
                \ELIF{$n \in (N_p - Call_p - \{e_p\})$}
                    \FOR{\textbf{each} $(m, d_3)$ such that $(n, d_2)\to (m, d_3) \in E^{\sharp}$}
                        \STATE \CALL{Propagate}{$(s_p, d_1) \to (m, d_3)$}
                    \ENDFOR
                \ENDIF
            \ENDWHILE
        \ENDPROCEDURE
        \end{algorithmic}
        \end{algorithm}