diff --git a/pub/dissertation/chapters/background.tex b/pub/dissertation/chapters/background.tex
index 0e45bdf..57bdd2b 100644
--- a/pub/dissertation/chapters/background.tex
+++ b/pub/dissertation/chapters/background.tex
@@ -88,10 +88,21 @@
 % TODO add quick overview of what Formal Methods are
 % Potential resource: https://shemesh.larc.nasa.gov/fm/fm-what.html
 
-\subsection{History}
-
-
-\subsection{Application}
+\begin{itemize}
+  \item Formal methods is a mathematical technique that can be used towards the
+    verification of a system~\cite{nasa:formal}
+  \item This can be used to verify correctness of all the inputs in a system~\cite{nasa:formal}
+  \item Hence, as dealing with safety, it would be beneficial to have
+    the logic of this testing tool verified, to avoid bugs and misleading results
+  \item Airbus also uses formal methods in their avionics systems validation and
+    verification process~\cite{airbus:formal}
+  \item Some examples where Airbus used formal methods was during the development
+    for the Airbus A380, where they used it for proof of absence of stack overflows
+    and analysis of the numerical precision and stability of floating-point operators
+    to name a few~\cite{airbus:formal}
+  \item There are a multitude of specification languages, each of them
+    having their own reasons % TODO don't know if this should be included
+\end{itemize}
 
 
 %%%%% SOLUTION STACK %%%%%
diff --git a/pub/dissertation/dissertation.pdf b/pub/dissertation/dissertation.pdf
index 4697a57..afbce68 100644
Binary files a/pub/dissertation/dissertation.pdf and b/pub/dissertation/dissertation.pdf differ
diff --git a/pub/dissertation/dissertation.sum b/pub/dissertation/dissertation.sum
index b60bc6a..8982cab 100644
--- a/pub/dissertation/dissertation.sum
+++ b/pub/dissertation/dissertation.sum
@@ -1 +1 @@
-4915
+5035
diff --git a/pub/dissertation/references.bib b/pub/dissertation/references.bib
index abd5379..82b1c40 100644
--- a/pub/dissertation/references.bib
+++ b/pub/dissertation/references.bib
@@ -47,8 +47,27 @@
   url = {https://ntrs.nasa.gov/citations/20160013263},
 }
 
+@online{nasa:formal,
+  author = {NASA Langley Formal Methods Research Program},
+  title = {Langley Formal Methods Program • What is Formal Methods},
+  url = {https://shemesh.larc.nasa.gov/fm/fm-what.html},
+  urldate = {2024-05-20}
+}
+
+@inproceedings{airbus:formal,
+  author={Laurent, Odile},
+  booktitle={2010 Third International Conference on Software Testing, Verification and Validation}, 
+  title={Using Formal Methods and Testability Concepts in the Avionics Systems Validation and Verification (V\&V) Process}, 
+  year={2010},
+  volume={},
+  number={},
+  pages={1-10},
+  keywords={System testing;Aerospace electronics;Automatic testing;Formal specifications;Aircraft;Software testing;Ground support;Assembly systems;Fault diagnosis;Automation;Formal methods;testing strategy;automatic test case generation;validation and verification},
+  doi={10.1109/ICST.2010.38}
+}
+
 @book{manifesto,
-  author = {Atul Gawande},
+  author = {Gawande, Atul},
   title = {The Checklist Manifesto: How To Get Things Right},
   publisher = {Profile Books},
   edition = {Main Edition},