First draft of Objectives

Chapters/Chapter04.tex

@@ -4,10 +4,56 @@
 
 \section{Objectives and Expected Results}
 
-\subsection{Unconstrained variable propagation for quantified bit-vectors}
+\subsection{Unconstrained variable propagation for quantified
+  bit-vectors}
+Simplifications using unconstrained variables can be extended to
+quantified formulas. However, in the quantified setting, constraints
+can be induced also by the order of the quantified variables. We have
+hypothesis of the necessary condition for the quantified variable to
+be unconstrained and we have implemented an proof-of-concept
+simplification procedure using unconstrained variables for the
+quantified bit-vector formulas. Although the initial experimental
+results, conducted on the formula from the semi-symbolic model checker
+\SymDivine look promissing, the formal proof of the correctnes is not
+yet complete.
+
+Furthermore, we suggest simplifications even for term in the form
+$k \times x$ with odd values of $x$. If $x$ has bit-width $n$, $i$ is
+the largest number such that $2^i$ which divides the constant $k$ and
+the value $x$ is unconstrained, the term $k \times x$ can be rewritten
+to $extract_0^{n-i}(x) \cdot 0^i$. This approach can possibly be extended
+to the multiplication of two variables from one is unconstrained and
+further generalized. We plan to prove the correctness of these rules
+and develop a formal framework to classify such rewrite rules.
+
 \subsection{Complexity of BV2}
-\subsection{Hybrid approach to quantified bit-vectors}
+
 \subsection{Symbolic solver for quantified bit-vectors}
+We also plan to further develop the implemented symbolic \smt solver
+for quantified bit-vecors Q3B. Besides implementing the proposed
+simplifiactions using unconstrained variables, we plan to add support
+of uninterpreted functions and theory of arrays to the Q3B. Also used
+approximations are right now very simple and could benefit from better
+refinement of the approximation in the case that the current
+approximation is too coarse.
+
+\subsection{Hybrid approach to quantified bit-vectors}
+Although our results with the symbolic \smt solver for quantified
+bit-vectors look promissing, standard \smt solvers still perform
+better on simple queries and on queries containing
+multiplication. Therefore, I want to develop a hybrid approach to \smt
+solving of quantified bit-vector formulas, which combines strengths of
+both of these approaches. For example, a part of the quantified
+formula without multiplication can be converted to the \bdd, which can
+be used to guide the model search in the model-based quantifier
+instantiation. One possible way of achieving this is adding \bdd based
+representation of sets of assignments to the \mcbv solver developed by
+Zeljić et al. The \bdd representation can be added to current
+over-approximations by bit-patterns and arithmetic intervals.
+
+As the part of my PhD study, also an implementation of a proposed
+hybrid approach and its evaluation on the representative set of
+benchmark is expected.
 
 \newpage
 \section{Progression Schedule}
@@ -16,6 +62,8 @@ The plan of my future study and research activities is following:
 \begin{description}[style=nextline,leftmargin=0.8cm]
 \item [now -- January 2017] Extending unconstrained variable
   propagation to quantified formulas and to non-linear multiplication.
+\item [now -- January 2019] Improvements and mantaining of the
+  developed symbolic \smt solver Q3B.
 \item [January 2017] Doctoral exam and defence of this thesis proposal.
 \item [January 2017 -- May 2017] Proving a precise complexity class of
   the quantfied bit-vector formulas without uninterpreted functions