diff --git a/verfahren.pdf b/verfahren.pdf
index 80a1e38..3fcc934 100644
Binary files a/verfahren.pdf and b/verfahren.pdf differ
diff --git a/verfahren.tex b/verfahren.tex
index 4a63e26..a2430d2 100644
--- a/verfahren.tex
+++ b/verfahren.tex
@@ -402,11 +402,51 @@
 \subsection{DFA-Ansatz zur intraprozeduralen, fluss-sensitiven may-Analyse nach Muchnick}
 \begin{itemize}
 	\item Vorwärtsproblem mit minimalen Grundblöcken
-	\item Sprachabhängige lokale Flussfunktionen für unmittelbare Auswirkungen pro Instruktion (Sammler/Gatherer): \begin{itemize}
-		\item TODO (VL-07)
+	\item Sprachabhängige lokale Flussfunktionen für unmittelbare Auswirkungen pro Instruktion (Sammler/Gatherer), hier für C: \begin{itemize}
+		\item Programmpunkt $P$: Kante in KFG der minimalen Grundblöcke
+		\item $\mathit{stmt}(P)$: Instruktion an Quelle der $P$-Kante
+		\item o.B.d.A. Annahme, dass jeder Programmpunkt $P$ nur einen Vorgänger $P'$ besitzt (synthetisch für Vorverarbeitung erzeugen)
+		\item Speicherstelle des Datums $x$ an Punkt $P$ $\mathit{mem}_P(x)$ initialisieren auf \begin{itemize}
+			\item $\mathit{star}(o)$: Für $o$ statisch allozierter Speicherbereich
+			\item $\mathit{anon}$: Dynamisch allozierter Speicherbereich
+		\end{itemize}
+		\item $\mathit{any}$ als Menge aller Speicherbereiche
+		\item Notation für Funktionen des Aliaswissens:\begin{itemize}
+			\item $\mathit{ptr}_P(x)$: Menge der Speicherstellen, auf die $x$ an $P$ zeigen kann
+			\item $\mathit{ref}_P(x)$: Menge der Speicherstellen, die an $P$ von $x$ über beliebig viele Derefenzierungen erreicht werden können
+			\item $\mathit{ovr}_P(x)$: Menge der Speicherstellen, die $x$ an $P$ überdecken kann
+		\end{itemize}
+		\item Flussfunktionen:\begin{itemize}
+			\item \texttt{x = \&a}: $\mathit{ptr}_P(x) = \lbrace\mathit{mem}_P(a)\rbrace = \lbrace\mathit{mem}_{P'}(a)\rbrace$
+			\item \texttt{x = y}: \begin{equation*}
+				\mathit{ptr}_P(x) = \mathit{ptr}_P(y) = \begin{cases*}
+					\lbrace \mathit{mem}_0(*y)\rbrace & falls $P' = 0$\\
+					\mathit{ptr}_{P'}(y) & sonst
+				\end{cases*}
+			\end{equation*}
+			\item \texttt{*x = a}: $\mathit{ptr}_P(x) = \mathit{ptr}_{P'}(x)$, zusätzlich wenn \texttt{*x} Zeiger $\mathit{ptr}_P(*x) = \mathit{ptr}_{P'}(*x) \cup \mathit{ptr}_{P'}(a)$
+			\item \texttt{f(...)}: \begin{itemize}
+				\item $G$: Menge der global sichtbaren Zeiger
+				\item $L$: Menge der lokalen Variablen im Aufrufer, deren Adresse berechnet wurde
+				\item $\forall x \in G \cup L:\, \mathit{ptr}_P(x) = \left(\cup_{g \in (G \cup \mathit{mem}(G))} \mathit{ref}_{P'}(g)\right) \cup \left(\cup_{l\in L} \mathit{ref}_{P'}(l)\right)$
+			\end{itemize}
+		\end{itemize}
 	\end{itemize}
 	\item Sprachunabhängiger Fixpunktpunktalgorithmus (Verbreiter/Propagator): \begin{itemize}
-		\item TODO (VL-07)
+		\item Initialisierung aller Zeigervariablen $x$ mit \begin{equation*}
+			\mathit{Ptr}(P, x) = \begin{cases*}
+				\emptyset & falls $P = 0$ und $x$ ist lokale Variable\\
+				\mathit{any} & falls $P = 0$ und $x$ ist globale Variable\\
+				\lbrace \mathit{mem}_0(*x)\rbrace & falls $P = 0$ und $x$ ist Parameter\\
+				\emptyset & sonst
+			\end{cases*}
+		\end{equation*}
+		\item Berechnung des Aliaswissens:\begin{equation*}
+			\mathit{Ptr}(P, x) = \begin{cases*}
+				\mathit{ptr}_P(x) & falls $\mathit{stmt}(P)$ Zeiger $x$ beeinflusst\\
+				\mathit{Ptr}(P',x) & sonst
+			\end{cases*}
+		\end{equation*}
 	\end{itemize}
 \end{itemize}