diff --git a/RV2015/Related.tex b/RV2015/Related.tex index 91b653c..268057b 100644 --- a/RV2015/Related.tex +++ b/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 diff --git a/RV2015/Structure.tex b/RV2015/Structure.tex index 511a075..3afb883 100644 --- a/RV2015/Structure.tex +++ b/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}. diff --git a/RV2015/conclusion.tex b/RV2015/conclusion.tex index 55b74d8..39547d6 100644 --- a/RV2015/conclusion.tex +++ b/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. diff --git a/RV2015/intro.tex b/RV2015/intro.tex index 9208b78..fbb1e2a 100644 --- a/RV2015/intro.tex +++ b/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 diff --git a/RV2015/prover.tex b/RV2015/prover.tex index 86a62ac..bdde7e5 100644 --- a/RV2015/prover.tex +++ b/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