related work + conclusion

2 files changed, 2 insertions, 2 deletions

diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex
index 848f65a..a1ecad2 100644
--- a/chapters/background/01-neural-networks.tex
+++ b/chapters/background/01-neural-networks.tex
@@ -2,7 +2,7 @@
 \label{sec:neural-networks}
 
 A neural network is a computational model inspired by biological neural networks. It consists of
-connected nodes called neuron, introduced in its early form by Rosenblatt et al.~\cite{rosenblatt1958perceptron}.
+connected nodes called neuron, introduced in its early form by Rosenblatt~\cite{rosenblatt1958perceptron}.
 \textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using
 backpropagation as popularized by Rumelhart et al.~\cite{rumelhart1986learning}.
 
diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex
index bd90559..a55d54d 100644
--- a/chapters/background/03-satisfiability-modulo-theories.tex
+++ b/chapters/background/03-satisfiability-modulo-theories.tex
@@ -19,6 +19,6 @@ To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disj
     (x > 0 \land y = x) \lor (x \le 0 \land y = 0)
 \end{equation}
 For a network with $N$ ReLU neurons, there are up to $2^N$ possible activation patterns. Solving the
-verification property requires the SMT solver, such as Z3 presented by Demura et al.~\cite{demoura2008z3},
+verification property requires the SMT solver, such as Z3 presented by De Moura et al.~\cite{demoura2008z3},
 to implicitly explore this branching search space.