Commit baf0af47 authored by Martin Jonáš's avatar Martin Jonáš
Browse files

Some changes in Objectives

parent a2b78be4
......@@ -4,6 +4,43 @@
\section{Objectives and Expected Results}
\subsection{Symbolic solver for quantified bit-vectors}
I plan to further develop the implemented symbolic \smt solver for
quantified bit-vecors Q3B. Besides implementing the proposed
simplifiactions using unconstrained variables, I plan to add support
of uninterpreted functions and theory of arrays, which are highly
desirable for the usage in program verification. I also want to
implement a support for extracting unsatisfiable cores from the
intermediate \bdds, which were produced during the computation of the
solver.
Additionally, approximations implemented are right now very simple and
could benefit from better refinement of the approximation in the case
that the current approximation is too coarse.
Moreover, we want to implement other variants of decision diagrams
such as zero-suppressed decision diagrams introduced by ??? and
algebraic decision diagrams introduced by ??? and experimentally
evaluate their effect on the performance of the \smt solver.
\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 the 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.
\subsection{Unconstrained variable propagation for quantified
bit-vectors}
Simplifications using unconstrained variables can be extended to
......@@ -21,39 +58,30 @@ 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.
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}
As was explained in section ???, the precise complexity of quantified
bit-vector formulas with binary-encoded bit-widths and without
uninterpreted functions is not known. It is known to be in \EXPSPACE
and to be \NEXPTIME-hard. However, a class for which the problem is
complete is not known.
\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.
Acording to our investigation, it is probably complete for neither of
those complexity classes. We are working on a proof which shows that
BV2 is complete for the class of problems solvable by the
\emph{alternating Turing machine} (\atm) with the exponential space
and \emph{polynomial number of alternations} with respect to log-space
reduction. This class is usually denoted as \AEXPTIMEp and is known to
be in between \EXPSPACE and \NEXPTIME. However, whether any of the
inclusions is proper is not known.
\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.
Expected result is a paper published at an international conference or
in a journal.
\newpage
\section{Progression Schedule}
......
......@@ -29,6 +29,8 @@
\newcommand{\EXPSPACE}{\textsf{EXPSPACE}\xspace}
\newcommand{\NEXPTIME}{\textsf{NEXPTIME}\xspace}
\newcommand{\NNEXPTIME}{\textsf{2-NEXPTIME}\xspace}
\newcommand{\AEXPTIMEp}{\textsf{AEXPTIME(poly)}\xspace}
\newcommand{\atm}{\textsc{atm}\xspace}
\newcommand{\state}[2]{\ensuremath{#1 \; || \; #2}\xspace}
\newcommand{\dec}[1]{\ensuremath{#1^\bullet}}
......@@ -42,7 +44,7 @@
\newcommand{\sort}[1]{\ensuremath{[#1]}}
\newcommand{\extract}[2]{\ensuremath{\texttt{extract}^{#1}_{#2}}}
\newcommand{\SymDivine}{\textsf{SymDIVINE}}
\newcommand{\SymDivine}{\textsf{SymDIVINE}\xspace}
\newcommand{\der}{\textsc{der}\xspace}
\newcommand{\teuf}{\ensuremath{T_\mathit{EUF}}\xspace}
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment