typos

RV2015/Related.tex

@@ -47,7 +47,7 @@ \section{Related Work}\label{sec:related}
 checking tools used in \texttt{Copilot-Kind}.  The work that is most
 relevant the research presented in this paper is the application of
 the Kind model checking tool to verify Lustre programs~\cite{Hagen08}.
-Kind and its most recent incarnation~\cite{kind2}is designed to model
+Kind and its most recent incarnation~\cite{kind}is designed to model
 check Lustre programs and due to the similarities of the Copilot a
 Lustre we targeted the Kind2 prover to be one of our back ends as
 well.  Yet, to the best of our knowledge, the Boyer-Moore majority

RV2015/Structure.tex

@@ -108,8 +108,8 @@ \subsection{Approximating a specification}
 \subsection{The Light prover and the IL format} 
 
 Our homegrown prover relies on an intermediate representation format called
-{IL}. An IL specification mostly consists in a list of quantifier-free equations
-over integer sequences. These equations contains a free variable $n$ which is
+{IL}. An IL specification mostly consists of a list of quantifier-free equations
+over integer sequences. These equations contain a free variable $n$ which is
 implicitly universally quantified. The IL format is similar to the one used by Hagen~\cite{HagenPhD}.
 
 

RV2015/conclusion.tex

@@ -22,40 +22,10 @@ \section{Future Work and Conclusion}\label{sec:conclusion}
 
 Verified  monitors are by no means sufficient for achieving assured RV,
 since a safety case is far more encompassing, but it is a necessary
-<<<<<<< HEAD
 condition.  Having applied our tool to rather
 sophisticated monitors,  future extensions are planned.  Of particular
 interest is an interface to 
 MetiTarski~\cite{AkbarpourPaulson}. This would allow us to discharge
 proofs of invariants involving real-valued special functions, which
-would arise quite often in the domain of cyber-physical systems.
-
-\subsubsection{Assurance} The reported efforts have
-primarily focused on verifying invariant properties of monitors using
-$k-$induction. Our solution is not a panacea as any model checking
-solution is subject to the well known state explosion problem, but 
-the results in verifying both simple and relatively complex monitors
-are promising. 
-
-\subsubsection{Efficacy of the Embedded DSL Approach} First, we have
-demonstrated that the embedded DSL approach is powerful and flexible
-in that we were able to extend the Copilot RV framework with
-verification capabilities. Being embedded in a  higher-order functional language
-facilitated the creation of  a number of features such as our proof
-scheme capability. The fact Copilot is a Haskell based eDSL yielded
-very  concise properties. For instance, in Section~\ref{sec:mvote}
-the power of higher-order expression is well illustrated in 
-function  \texttt{forAllCst} for the
-serial Boyer-Moore example in that it  uses both a  a \texttt{fold}
-and a \texttt{map} operator to model finite conjunctions. 
-
-
-\subsubsection{Future Work} In the near term, we continue our
-collaboration with the Kind2 team as the prover gets more
-sophisticated and provides a more flexible interface. Given we already
-output SMTLib format in order to interface with Yices, we will
-investigate connecting to other provers that use that input
-format. Finally, we shall interface the verification with
-MetiTarski~\cite{AkbarpourPaulson}, which would allow us to discharge
-proofs of invariants involving real-valued special functions.
+arise quite often in the domain of cyber-physical systems.
 

RV2015/intro.tex

@@ -42,8 +42,8 @@ \section{Introduction}\label{sec:intro}
 model-checker~\cite{Sheeran00,EenS03} for Copilot called
 \texttt{copilot-kind}. More precisely, \texttt{copilot-kind} is a model-checking
 framework for Copilot, with two existing backends including a lightweight
-implementation of $k$-induction using Yices~\cite{} and a backend based on
-\emph{Kind2}, implementing both $k$-induction and the IC3~algorithm~\cite{}.
+implementation of $k$-induction using Yices~\cite{Dutertre:cav2014} and a backend based on
+\emph{Kind2}, implementing both $k$-induction and the IC3~algorithm~\cite{Somenzi-FMCAD11}.
 
 After providing a brief introduction to Copilot in Section~\ref{sec:co-intro}
 and to SMT-based $k$-induction in Section~\ref{sec:background}, we introduce

RV2015/prover.tex

@@ -1,7 +1,7 @@
 \section{Copilot Prover Interface}~\label{sec:prover} 
 The \texttt{copilot-kind} model-checker is an extensible interface to multiple
 provers used to verify safety properties of Copilot
-programs. Currently, two backends for \texttt{copiot-kind have been implemented}: the first is a
+programs. Currently, two backends for \texttt{copiot-kind} have been implemented: the first is a
 homegrown prover we call ``the light prover'' built on top of
 Yices~\cite{Dutertre:cav2014} and the second is the Kind2 model checker being developed at
 the University of Iowa~\cite{kind}.
@@ -110,7 +110,7 @@ \subsubsection{Combining Provers.}\label{combining-provers}
 hold as well as reflexivity, antisymmetry, and transitivity. (Merging provers
 that handles non-termination within a bound is future work.)
 
-In practice, we used the following prover in the examples of Section~\ref{sec:example} :
+In practice, we used the following prover in the examples of Section~\ref{sec:example}:
 \begin{lstlisting}[frame=single]
 prover = lightProver def {kTimeout = 5} `combine` kind2Prover def
 \end{lstlisting}
@@ -143,7 +143,7 @@ \subsubsection{Proof Schemes.}\label{proof-schemes}
 \end{lstlisting}
 A \emph{proof scheme} is a chain of
 primitives schemes glued by the $\texttt{\textgreater{}\textgreater{}}$
-operator to combine proofs, and in particular, provide lemmas. The available primitives are :
+operator to combine proofs, and in particular, provide lemmas. The available primitives are:
 
 \begin{itemize}
 \itemsep1pt\parskip0pt\parsep0pt