diff --git a/Lectures/L29_IntroductionToVerification/DeleteCorrect.java b/Lectures/L29_IntroductionToVerification/DeleteCorrect.java
new file mode 100644
index 0000000000000000000000000000000000000000..e1fd95834b8c976c5ebc924445b2a48fbd4b6f15
--- /dev/null
+++ b/Lectures/L29_IntroductionToVerification/DeleteCorrect.java
@@ -0,0 +1,11 @@
+   public static void del(int i)
+   {
+     int j;
+
+     for (j = i; j < (length - 1); j++)
+     {
+       s[j] = s[j+1];
+     }
+
+     length = length - 1;
+   }
\ No newline at end of file
diff --git a/Lectures/L29_IntroductionToVerification/DeleteIncorrect.java b/Lectures/L29_IntroductionToVerification/DeleteIncorrect.java
new file mode 100644
index 0000000000000000000000000000000000000000..df93cf93810c7ef369da3077b4826741a582865e
--- /dev/null
+++ b/Lectures/L29_IntroductionToVerification/DeleteIncorrect.java
@@ -0,0 +1,11 @@
+   public static void del(int i)
+   {
+     int j;
+
+     for (j = i; j <= (length - 1); j++)
+     {
+       s[j] = s[j+1];
+     }
+
+     length = length - 1;
+   }
\ No newline at end of file
diff --git a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..bee5542aa354e3a19424b1b2c5fcec1754f5be97
Binary files /dev/null and b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf differ
diff --git a/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex
new file mode 100755
index 0000000000000000000000000000000000000000..804f37a36571381366c50d0a8fbd45a81cd82e32
--- /dev/null
+++ b/Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex
@@ -0,0 +1,352 @@
+%\documentclass[t,12pt,numbers,fleqn,handout]{beamer}
+\documentclass[t,12pt,numbers,fleqn]{beamer}
+
+\usepackage{pgfpages} 
+\usepackage{hyperref}
+\hypersetup{colorlinks=true,
+    linkcolor=blue,
+    citecolor=blue,
+    filecolor=blue,
+    urlcolor=blue,
+    unicode=false}
+\urlstyle{same}
+
+\usepackage{hhline}
+\usepackage{booktabs}
+\usepackage{multirow}
+\usepackage{multicol}
+\usepackage{array}
+\usepackage{listings}
+
+\usepackage{amssymb}
+\usepackage{amsmath}
+
+\useoutertheme{split} %so the footline can be seen, without needing pgfpages
+
+% \pgfpagesuselayout{resize to}[letterpaper,border
+% shrink=5mm,landscape] %if this is uncommented, the hyperref links do not work
+
+\mode<presentation>{}
+
+\input{../def-beamer}
+
+\newcommand{\topic}{29 Introduction to Verification}
+
+\input{../titlepage}
+
+\begin{document}
+
+\input{../footline}
+
+\lstset{language=java,breaklines=true,showspaces=false,showstringspaces=false,breakatwhitespace=true}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Introduction to Verification}
+
+\begin{itemize}
+\item Today's slide are partially based on slides by Dr.\ Wassyng, Ghezzi et al
+\item Administrative details
+\item pointInRegion(p)
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Administrative Details}
+
+\begin{itemize}
+
+\item Investigating 9 academic integrity cases for A2
+
+\item A3 deadlines
+\begin{itemize}
+\item Part 2 - Code: due 11:59 pm Mar 20
+\item {Part 1 spec available in repo}
+\item \structure{Change of $<$ to $\leq$ in natural language and spec}
+\end{itemize}
+
+\item A4
+\bi
+\item Your own design and specification
+\item Due April 3 at 11:59 pm
+\ei
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{A Table for pointInRegion(p)}
+
+\begin{itemize}
+
+\item Consider all of the cases
+\item Draw a picture
+\item Short form notation
+\begin{itemize}
+\item $px = p.\mbox{xcoord()}$
+\item $py = p.\mbox{ycoord()}$
+\item $llx = \mathit{lower\_left}.\mbox{xcoord()}$
+\item $lly = \mathit{lower\_left}.\mbox{ycoord()}$
+\item $llxw = \mathit{lower\_left}.\mbox{xcoord()} + \mathit{width}$
+\item $llyh = \mathit{lower\_left}.\mbox{ycoord()} + \mathit{height}$
+\item T = Constants.TOLERANCE
+\end{itemize}
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}[plain]
+%\frametitle{A Table for Assignment 4, Part 2, pointInRegion(p)}
+
+\begin{tabular}{|p{2.cm}|p{2.8cm}|p{5.3cm}|}
+\hhline{~|~|-|}
+\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
+\hhline{|-|-|-|}
+{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
+\mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$lly \leq py \leq llyh$} & {$(llx - px) \leq \mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
+\hhline{-|-|-|}
+{$llx \leq px \leq llxw$} & {$py < lly$} & {$(lly-py) \leq\mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$lly \leq py \leq llyh$} & {$\mbox{True}$}\\
+\hhline{|~|-|-|}
+~ & {$py > llyh$} & {$(py - llyh) \leq \mbox{T}$}\\
+\hhline{-|-|-|}
+{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
+\mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$lly \leq py \leq llyh$} & {$(px-llxw) \leq \mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw,llyh)) \leq \mbox{T}$}\\
+\hhline{-|-|-|}
+
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Seven Cases}
+
+\begin{tabular}{|p{2.cm}|p{2.8cm}|p{5.3cm}|}
+\hhline{~|~|-|}
+\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
+\hhline{|-|-|-|}
+{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
+\mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$lly \leq py \leq llyh$} & {$(llx - px) \leq \mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
+\hhline{|-|-|-|}
+\multicolumn{2}{|l|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
+\mbox{T})$}\\
+\hhline{|-|-|-|}
+{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
+\mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$lly \leq py \leq llyh$} & {$(px-llxw) \leq \mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
+\hhline{-|-|-|}
+
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Six Cases}
+
+\begin{tabular}{|p{2.5cm}|p{2.5cm}|p{5.1cm}|}
+\hhline{~|~|-|}
+\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
+\hhline{|-|-|-|}
+{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
+\mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
+\hhline{|-|-|-|}
+\multicolumn{2}{|l|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
+\mbox{T})$}\\
+\hhline{|-|-|-|}
+{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
+\mbox{T}$}\\
+\hhline{|~|-|-|}
+~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
+\hhline{-|-|-|}
+\multicolumn{2}{|l|}{{$lly \leq py \leq llyh$}} & {$(llx-\mbox{T}) \leq px \leq (llxw +
+\mbox{T})$}\\
+\hhline{|-|-|-|}
+
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Three Cases}
+
+\begin{tabular}{|p{2.5cm}|p{2.5cm}|p{5.1cm}|}
+\hhline{~|~|-|}
+\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
+\hhline{|-|-|-|}
+\multicolumn{2}{|p{5cm}|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
+\mbox{T})$}\\
+\hhline{|-|-|-|}
+\multicolumn{2}{|p{5cm}|}{{$lly \leq py \leq llyh$}} & {$(llx-\mbox{T}) \leq px \leq (llxw +
+\mbox{T})$}\\
+\hhline{|-|-|-|}
+\multicolumn{2}{|p{5cm}|}{{$\neg(llx \leq px \leq llxw) \wedge \neg(lly \leq py \leq llyh)$}} &
+{$\mbox{min}[p.\mbox{dist}(\mbox{PointT}(llx, lly)),$ $p.\mbox{dist}(\mbox{PointT}(llxw, lly)),$
+$p.\mbox{dist}(\mbox{PointT}(llx, llyh)),$ 
+$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) ] \leq \mbox{T}$}\\
+\hhline{|-|-|-|}
+
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Nine Cases, but 2D}
+
+\bi
+\item \structure{How would you write all 9 cases, but with a tabular form that
+    closely matches the original 2D problem description?}
+\ei
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Outline of Verification Topics}
+
+\begin{itemize}
+
+\item What are the goals of verification?
+\item What are the main approaches to verification?
+\begin{itemize}
+\item What kind of assurance do we get through testing?
+\item How can testing be done systematically?
+\item How can we remove defects (debugging)?
+\end{itemize}
+\item What are the main approaches to software analysis?
+\item Informal versus formal analysis
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Testing on Assignment 1 to 4}
+
+\begin{itemize}
+
+\item Limited guidance on test case selection
+\item Improved test cases would have improved the results
+\item Consider the method for deleting from a sequence of T (next slide)
+\item We are moving toward automated testing
+\item We have seen the advantages of regression testing
+\item Some have adopted the excellent strategy of test as you develop
+\begin{itemize}
+\item Helps isolate errors
+\item Does not leave testing to the end when there is no time to do it properly
+\item Helps improve the understanding of the problem and the program
+\end{itemize}
+\item Hopefully the experience on the assignments has motivated you to think more about testing
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Incorrect Version of Delete}
+
+Using \texttt{s = new T[MAX\_SIZE]}, for some type \texttt{T}
+
+\lstset{language=java,breaklines=true,showspaces=false,showstringspaces=false,breakatwhitespace=true}
+\noindent \lstinputlisting{DeleteIncorrect.java}
+
+What test cases will highlight the error?
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Correct Version of Delete}
+
+\lstset{language=java,breaklines=true,showspaces=false,showstringspaces=false,breakatwhitespace=true}
+\noindent \lstinputlisting{DeleteCorrect.java}
+
+Avoids potential ArrayIndexOutOfBoundsException Exception
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Need for Verification}
+
+\begin{itemize}
+
+\item Designers are fallible even if they are skilled and follow sound principles
+\item We need to build confidence in the software
+\item Everything must be verified, every required functionality, every required
+  quality, every process, every product, every document
+\item Even verification itself must be verified
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}
+\frametitle{Properties of Verification}
+
+\begin{itemize}
+
+\item May not be binary (OK, not OK)
+\begin{itemize}
+\item Severity of defect is important
+\item Some defects may be tolerated
+\item Our goal is typically acceptable reliability, not correctness
+\end{itemize}
+\item May be subjective or objective - for instance, usability, generic level of
+  maintainability or portability
+\item Even implicit qualities should be verified
+\begin{itemize}
+\item Because requirements are often incomplete
+\item For instance robustness, maintainability
+\end{itemize}
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
\ No newline at end of file