diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf
index 6cb8712..d3075ef 100644
Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ
diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex
index 97f6557..e0e774b 100644
--- a/semester4/fmfp/formal-methods-functional-programming-summary.tex
+++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex
@@ -131,6 +131,13 @@
 \input{parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex}
 % \input{parts/03_language-semantics/}
 
+\newsection
+\section{Modelling}
+\input{parts/04_modelling/00_intro.tex}
+\input{parts/04_modelling/01_promela/00_syntax.tex}
+% \input{parts/04_modelling/01_promela/}
+% \input{parts/04_modelling/}
+
 
 
 \end{document}
diff --git a/semester4/fmfp/parts/04_modelling/00_intro.tex b/semester4/fmfp/parts/04_modelling/00_intro.tex
new file mode 100644
index 0000000..9f76c87
--- /dev/null
+++ b/semester4/fmfp/parts/04_modelling/00_intro.tex
@@ -0,0 +1,23 @@
+\subsection{Model Checking}
+\begin{definition}[]{Model Checking}
+    Model checking is an automated technique that, given
+    a finite-state model of a system and a formal property,
+    systematically checks whether this property holds for
+    (a given state in) that model.
+\end{definition}
+
+Model checkers enumerate all possible states of a system, either through explicitly representing state through concrete values or symbolically through (boolean) formulas.
+
+They are primarily used to analyze system \bi{designs}, and not implementations and are often used to analyze deadlocks, the reachability of undesired states and protocol violations.
+
+
+\subsubsection{The Model Checking Process}
+The first and most important phase is the \bi{modeling phase}, where we model the system in the description language of the model checker (here Promela).
+It also includes formalizing the properties to be checked in said language.
+
+Next, we run the model checker to check the validity of the model. 
+In the case of this course, we use \texttt{spin}, and we can run a promela model using \texttt{spin -x <promela file>.pml},
+which wraps \texttt{spin -a <promela file>.pml}, \texttt{gcc <promela file>.c} and \texttt{./a.out} into a single command.
+
+After running, it is time to analyze the output of the model checker. If the property is violated, analyze the found conter example.
+If the mdeol is too large, it can happen that the checker runs out of memory. In that case, reduce the model and try again.
diff --git a/semester4/fmfp/parts/04_modelling/01_promela/00_syntax.tex b/semester4/fmfp/parts/04_modelling/01_promela/00_syntax.tex
new file mode 100644
index 0000000..2f177a9
--- /dev/null
+++ b/semester4/fmfp/parts/04_modelling/01_promela/00_syntax.tex
@@ -0,0 +1,2 @@
+\subsection{Promela}
+% p23