Multiple changes

  pages     = {48--64},

  year      = {2005}

}

@inproceedings{BC95,

  author    = {Randal E. Bryant and

               Yirng{-}An Chen},

  title     = {Verification of Arithmetic Circuits with Binary Moment Diagrams},

  booktitle = {{DAC}},

  pages     = {535--541},

  year      = {1995}

}

@inproceedings{Beaver,

  author    = {Susmit Jha and

               Rhishikesh Limaye and

               Sanjit A. Seshia},

  title     = {Beaver: Engineering an Efficient {SMT} Solver for Bit-Vector Arithmetic},

  booktitle = {Computer Aided Verification, 21st International Conference, {CAV}

               2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},

  pages     = {668--674},

  year      = {2009}

}

@inproceedings{Spear,

  author    = {Frank Hutter and

               Domagoj Babic and

               Holger H. Hoos and

               Alan J. Hu},

  title     = {Boosting Verification by Automatic Tuning of Decision Procedures},

  booktitle = {Formal Methods in Computer-Aided Design, 7th International Conference,

               {FMCAD} 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings},

  pages     = {27--34},

  year      = {2007}

}

@inproceedings{Sonolar,

  author    = {Jan Peleska and

               Elena Vorobev and

               Florian Lapschies},

  title     = {Automated Test Case Generation with SMT-Solving and Abstract Interpretation},

  booktitle = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011,

               Pasadena, CA, USA, April 18-20, 2011. Proceedings},

  pages     = {298--312},

  year      = {2011}

}

@inproceedings{STP,

  author    = {Vijay Ganesh and

               David L. Dill},

  title     = {A Decision Procedure for Bit-Vectors and Arrays},

  booktitle = {Computer Aided Verification, 19th International Conference, {CAV}

               2007, Berlin, Germany, July 3-7, 2007, Proceedings},

  pages     = {519--531},

  year      = {2007}

}

@inproceedings{HKVV15,

  author    = {Miika Hannula and

               Juha Kontinen and

               Jonni Virtema and

               Heribert Vollmer},

  title     = {Complexity of Propositional Independence and Inclusion Logic},

  booktitle = {Mathematical Foundations of Computer Science 2015 - 40th International

               Symposium, {MFCS} 2015, Milan, Italy, August 24-28, 2015, Proceedings,

               Part {I}},

  pages     = {269--280},

  year      = {2015}

}

 No newline at end of file

%************************************************

\chapter{Introduction}\label{ch:introduction}

% ************************************************

During the last decades, the area of solving \emph{propositinal

  satisfiability} (\sat)~\cite{DP09} and consequently the related area

of solving \emph{satisfiability modulo theories} (\smt)~\cite{BSST09}

has undergone steep development in both theory and practice. Achieved

advances of \smt solving opened new research directions in program

analysis and verification, where \smt solvers are now seen as standard

tools.

The task for an \smt solver is for a given first-order formula in a

given first-order theory decide, whether the formula is

satisfiable. Usually, if the formula is satisfiable, the \smt solver

also has the ability to provide its model. Modern \smt solvers support

wide range of different first-order theories -- for example, theories

of integers, real numbers, floating-point numbers, arrays, strings,

inductively defined data types, bit-vectors and various combinations

and framgents of these theories. From the software analysis and

verification point of view, a particularly important of these theories

is the theory of bit-vectors, which can be used to describing

properties of computer programs, since they usually use data-types of

bounded size instead of mathematical integers.

The benefit of describing properties of programs by bit-vector

formulas is twofold. Formulas in the bit-vector theory allow to model

the program's behavior precisely including possible arithmetic

overflows and underflows. Furthermore, in contrast to the theory of

integers, the satisfiability of bit-vector theory is decidable even if

the multiplication is allowed.

Therefore, quantifier-free bit-vector formulas are used in tools for

symbolic execution, bounded model checking, analysis of hardware

circuits, static analysis, or test generation. Most of the current

\smt solvers for the quantifier-free bit-vector formulas eagerly or

lazily translate the formula to the propositional logic

(\emph{bit-blasting}) and use an efficient \sat solver to decide its

satisfiability. Therefore, the efficiency of most of the \smt solvers

for such formulas is tightly connected to the efficiency of the \sat

solvers. Plenty of solvers for the quantifier-free bit-vector formulas

exist: Beaver~\cite{Beaver}, Boolector~\cite{Boolector},

CVC4~\cite{CVC4}, MathSAT5~\cite{MathSAT}, OpenSMT~\cite{OpenSMT},

Sonolar~\cite{Sonolar}, Spear~\cite{Spear}, STP~\cite{STP},

UCLID~\cite{LS04}, Yices~\cite{Yices}, or Z3~\cite{Z3}.

In some cases, quantifier-free formulas are not succint enough and

quantified formulas are necessary. Bit-vector quantified formulas

arise naturally for example in applications that generate loop

invariants, ranking functions, loop summaries, or that test equality

of two symbolic states. However, the \smt solvers' support of

quantified bit-vector logic is much more modest -- CVC4, Yices, and Z3

officially support quantifiers in bit-vector formulas. Recently,

quantifiers have been also implemented in an development version of

Boolector. All of these \smt solvers solve quantified bit-vector

formulas by some variant of quantifier-instantiation and using a

solver for quantifier-free formulas as an oracle.

In the last year, we have proposed a different approach. We have

implemented a symbolic solver Q3B, which is based on binary decision

diagrams, and have shown that it can not only compete with

state-of-the art \smt solvers, but outperforms them in many

cases~\cite{JS16}. However, \bdds are not a silver bullet; the

symbolic \smt solver fails on formulas containing non-trivial

multiplication and complex arithmetic. Therefore, as the aim of my PhD

study, I plan to develop a hybrid approach to solving quantified

bit-vectors, which combines symbolic representation by \bdds with

search techniques employed by existing state-of-the-art solvers. I

also plan to continue developing the symbolic solver Q3B itself,

namely improving its efficiency and adding support for features as

uninterpreted functions and arrays that are important in the software

verification.

The thesis proposal is organized as follows. Chapter~\ref{ch:sota}

summarizes the state of the art and is divided into six sections. The

first section introduces necessary background and notations from

propositional logic and first-order logic. The second section

describes approaches to solving propositional satisfiability problem

and the third section describes approaches to solving satisfiability

modulo theories. The fourth and fifth sections are devoted to solving

quantifier-free and quantifed formulas over the theory of bit-vectors,

respectively. The final, sixth, section describes results about the

computational complexity of bit-vector

logics. Chapter~\ref{ch:achieved} describes results, which we have

achieved during the first two years of my PhD

study. Chapter~\ref{ch:aims} presents the aim of the thesis and states

plans remaining part of the PhD study.

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "../ClassicThesis"

%%% End:

Let $\P$ be a fixed finite set of propositional variables. For every

variable $x \in \P$ there are two literals -- a \emph{positive

  literal} $x$ and a \emph{negative literal} $\overline{x}$. For a

given literal $l$, we define $\neg l$ as $\overline{l}$ if $l$ is

positive and as $l$ if $l$ is negative. Literals $l$ and $\neg l$ are

called \emph{complementary}. A \emph{clause} is a finite disjunction

of literals. The empty clause is denoted by $\bot$. A formula in the

\emph{conjunctive normal form} (\cnf) is a finite conjunction of

clauses. If convenient, we use idempotence and commutativity of

disjunction and view clauses as sets of literals and therefore ignore

the order and multiple occurrences of literals. Similarly, if

convenient, we view \cnf formulas as sets of clauses. For example, we

write the formula $(x \vee \overline{y}) \wedge (\overline{x} \vee z)$

as the set $\{ \{ x , \overline{y} \}, \{ \overline{x}, z \} \}$.

given literal $l$, we define $\neg l$ as $\overline{l}$ if $l = x$ for

some variable $x$ and as $x$ if $l = \overline{x}$ for some variable

x. Literals $l$ and $\neg l$ are called \emph{complementary}. A

\emph{clause} is a finite disjunction of literals. The empty clause is

denoted by $\bot$. A formula in the \emph{conjunctive normal form}

(\cnf) is a finite conjunction of clauses. If convenient, we use

idempotence and commutativity of disjunction and view clauses as sets

of literals and therefore ignore the order and multiple occurrences of

literals. Similarly, if convenient, we view \cnf formulas as sets of

clauses. For example, we write the formula

$(x \vee \overline{y}) \wedge (\overline{x} \vee z)$ as the set

$\{ \{ x , \overline{y} \}, \{ \overline{x}, z \} \}$.

A \emph{partial assignment} $M$ is a set of literals that does not

contain complementary literals, i.e.

$\{ x, \overline{x} \} \subseteq M$ for no $x \in \P$. A literal $l$

is \emph{true} in the assignment $M$ if $l \in M$, \emph{false} in $M$

if $\neg l \in M$, and \emph{undefined} otherwise. A literal is

$\{ x, \overline{x} \} \not \subseteq M$ for all $x \in \P$. A literal

$l$ is \emph{true} in the assignment $M$ if $l \in M$, \emph{false} in

$M$ if $\neg l \in M$, and \emph{undefined} otherwise. A literal is

\emph{defined} in $M$ if it is true or false in $M$. We call an

assignment $M$ \emph{total} over $\P$ if all literals of $\P$ are

defined in $M$. A clause is \emph{true} in $M$ if at least one of its

\subsection{First-order logic and theories}

A \emph{signature} $\Sigma$ consists of a set of \emph{function

  symbols} $\Sigma^f$, a set of \emph{predicate symbols} $\Sigma^p$

and a non-negative number for each of these symbols called its

  symbols} $\Sigma^f$, a set of \emph{predicate symbols} $\Sigma^p$,

and for each of these symbols a non-negative number called its

\emph{arity}. Given a signature $\Sigma$, \emph{$\Sigma$-terms},

\emph{$\Sigma$-atoms}, \emph{$\Sigma$-literals},

\emph{$\Sigma$-clauses}, and \emph{$\Sigma$-formulas} are defined as

usual. We are using the logic with equality, i.e. the set of

$\Sigma$-atoms contains elements $t_1 = t_2$ for each pair of

$\Sigma$-terms $t_1, t_2$. If the signature is clear from the context,

we drop the $\Sigma$- prefix and speak only of terms, atoms, literals,

and so on. We call terms and formulas \emph{ground} if they contain no

free variables.

\emph{$\Sigma$-clauses}, \emph{$\Sigma$-formulas}, and

\emph{$\Sigma$-formulas in \cnf} are defined as usual. We are using

the logic with equality, i.e. the set of $\Sigma$-atoms contains

elements $t_1 = t_2$ for each pair of $\Sigma$-terms $t_1, t_2$.  We

call $\Sigma$-terms and $\Sigma$-formulas \emph{ground} if they

contain no free variables.

A \emph{$\Sigma$-structure} $\mathcal{A}$ consists of a non-empty set

$A$, the \emph{universe} of the structure, and an assignment

and to each predicate symbol $P \in \Sigma^p$ of arity $n$ assigns a

relation $P^\mathcal{A} \subseteq A^n$. Given a $\Sigma$-structure

$\mathcal{A}$, there exists a unique homomorphic extension of

$(\_)^\mathcal{A}$ to terms, which to each term $t$ assigns an element

$t^\mathcal{A} \in A$. In turn, using standard definitions, the

assignment $(\_)^\mathcal{A}$ can be further extended to assign a

truth value $\varphi^\mathcal{A} \in \{ \true, \false \}$ to each

formula $\varphi$. A $\Sigma$-structure $\mathcal{A}$ is said to

\emph{satisfy} a $\Sigma$-formula $\varphi$ if

$(\_)^\mathcal{A}$ to $\Sigma$-terms, which to each $\Sigma$-term $t$

assigns an element $t^\mathcal{A} \in A$. In turn, using standard

definitions, the assignment $(\_)^\mathcal{A}$ can be further extended

to assign a truth value $\varphi^\mathcal{A} \in \{ \true, \false \}$

to each $\Sigma$-formula $\varphi$. A $\Sigma$-structure $\mathcal{A}$

is said to \emph{satisfy} a $\Sigma$-formula $\varphi$ if

$\varphi^\mathcal{A} = \true$. In such case, the structure

$\mathcal{A}$ is also called a \emph{model} of the formula $\varphi$.

A \emph{$\Sigma$-theory} $\mathcal{T}$ is a class of

$\Sigma$-structures closed under isomorphisms and variable

reassignment. A ground $\Sigma$-formula is said to be

\emph{satisfiable in the $\Sigma$-theory $\mathcal{T}$}, or

reassignment. A $\Sigma$-formula is said to be \emph{satisfiable in

  the $\Sigma$-theory $\mathcal{T}$}, or

\emph{$\mathcal{T}$-satisfiable}, if there exists a $\Sigma$-structure

$\mathcal{A} \in \mathcal{T}$ such that $\mathcal{A}$ satisfies

$\varphi$. The structure $\mathcal{A}$ is then called a

\emph{$\mathcal{T}$-model} of $\varphi$. If $\varphi$ is a ground

$\Sigma$-formula and $\Gamma$ is a set of ground $\Sigma$-formulas, we

say that \emph{$\Gamma$ entails $\varphi$ in $\mathcal{T}$}, written

\emph{$\mathcal{T}$-model} of $\varphi$. If $\varphi$ is a

$\Sigma$-formula and $\Gamma$ is a set of $\Sigma$-formulas, we say

that \emph{$\Gamma$ entails $\varphi$ in $\mathcal{T}$}, written

$\Gamma \models_\mathcal{T} \varphi$, if every $\Sigma$-structure that

satisfies all formulas in $\Gamma$ also satisfies $\varphi$. If

$\emptyset \models_\mathcal{T} \varphi$ for a ground $\Sigma$-formula

$\emptyset \models_\mathcal{T} \varphi$ for a $\Sigma$-formula

$\varphi$, the formula $\varphi$ is called \emph{$\mathcal{T}$-valid}

or a \emph{theory lemma}. A set $\Gamma$ of ground $\Sigma$-formulas

is called \emph{$\mathcal{T}$-inconsistent}, if

or a \emph{theory lemma}. A set $\Gamma$ of $\Sigma$-formulas is

called \emph{$\mathcal{T}$-inconsistent}, if

$\Gamma \models_{\mathcal{T}} \bot$.

% If $\varphi$

In the rest of this chapter, we consider only theories for which the

satisfiability of conjunctions of literals is decidable and we call

any decision procedure for conjunctions of $\mathcal{T}$-literals a

$\mathcal{T}$-\emph{solver}.

$\mathcal{T}$-\emph{solver}. Moreover, if the signature or the theory

is clear from the context, we drop the respective $\Sigma$- or

$\mathcal{T}$- prefixes.

% In the following text, we suppose the knowledge of a standard

% first-order logic and model theory, which is given for example by

solvers relies on \emph{branching heuristics}, which select the next

decision variable during the search. Multiple branching heuristics

have been proposed~\cite{BF15branching} and the majority of modern

\sat solver are using VSIDS heuristic~\cite{MMZZM01}, which prefers

\sat solver are using \vsids heuristic~\cite{MMZZM01}, which prefers

branching on the variables that have appeared in the biggest number of

recent conflicts. More recently, new branching heuristics based on

learning rate have been proposed and shown to outperform the currently

used VSIDS branching heuristic~\cite{LGPC16}.

used \vsids branching heuristic~\cite{LGPC16}.

Another important part of modern \sat solvers are dynamic restarts,

which allow restarting the search from scratch in hope that clauses

solver~\cite{Minisat} has been experimentally evaluated by Katebi,

Sakallah, and Marques-Silva~\cite{KSM11}. The experimental evaluation

shows that the most important from the mentioned techniques is

clause-learning, followed by the VSIDS branching heuristic.

clause-learning, followed by the \vsids branching heuristic.

\subsection{Other approaches to \sat}

Aside from conflict-driven \sat algorithms, other variants of

\item the theory of \emph{linear real arithmetic} over the signature

  $\{ +, \leq \}$, which consists of all structures isomorphic to real

  numbers with the function $+$ and the relation $\leq$;

\item the theory of \emph{real arithmetic} \marginpar{In contrast to

    real arithmetic, integer arithmetic with multiplication was shown

    to be undecidable by Gödel.} over the signature

\item the theory of \emph{real arithmetic} over the signature

  $\{ +, \times, \leq \}$, which consists of all structures isomorphic

  to real numbers with functions $+$ and $\times$ and the relation

  $\leq$;

fragment of the first-order logic, which is well known to be

\NEXPTIME-complete~\cite{WHD13}. The class of effectively

\marginpar{The class of effectively propositional formulas is also

  known the Bernays--Schönfinkel class.} propositional formulas

  known as the Bernays--Schönfinkel class.} propositional formulas

consists only of formulas in form $\exists^*\forall^*\varphi$, where

$\varphi$ does not contain any quantifiers or function symbols.

and uninterpreted functions was investigated by Kovásznai et

al.~\cite{KFB12}. Reencoding of all bit-widths to unary shows that

UFBV2 is in \NNEXPTIME. For the lower bound, Kovásznai et al. present

a reduction of a instance of a \emph{domino tiling

a reduction of an instance of a \emph{domino tiling

  problem}~\cite{Chl84} that is known to be \NNEXPTIME-hard.

%*****************************************j

%************************************************

\chapter{Achieved Results}\label{ch:achieved results} % $\mathbb{ZNR}$

\chapter{Achieved Results}\label{ch:achieved} % $\mathbb{ZNR}$

%************************************************

\section{Symbolic approach to quantified bit-vectors}

sign-extensions.

\begin{figure}[tb]

  \checkoddpage

  \edef\side{\ifoddpage l\else r\fi}

  \makebox[\textwidth][\side]{

    \begin{minipage}[b]{\fullwidth}

      \begin{tabularx}{\textwidth}{c X c}

        \newcolumntype{C}{>{\centering\arraybackslash}p{2.5ex}}

        \newcolumntype{C}{>{\centering\arraybackslash}p{2ex}}

        \begin{tabular}{ | C | C | C | C | C | C | }

          \hline

          0 & 0 & 0 & $a_2$ & $a_1$ & $a_0$ \\

          \hline

        \end{tabular}

            &&

               \newcolumntype{C}{>{\centering\arraybackslash}p{2.5ex}}

               \newcolumntype{C}{>{\centering\arraybackslash}p{2ex}}

               \begin{tabular}{ | C | C | C | C | C | C | }

                 \hline

                 $a_2$ & $a_2$ & $a_2$ & $a_2$ & $a_1$ & $a_0$ \\

               \end{tabular}

        \\ zero-extension && sign-extension

        \\ [1ex]

        \newcolumntype{C}{>{\centering\arraybackslash}p{2.5ex}}

        \newcolumntype{C}{>{\centering\arraybackslash}p{2ex}}

        \begin{tabular}{ | C | C | C | C | C | C | }

          \hline

          $a_5$ & $a_4$ & $a_3$ & 0 & 0 & 0 \\

          \hline

        \end{tabular}

            &&

               \newcolumntype{C}{>{\centering\arraybackslash}p{2.5ex}}

               \newcolumntype{C}{>{\centering\arraybackslash}p{2ex}}

               \begin{tabular}{ | C | C | C | C | C | C | }

                 \hline

                 $a_5$ & $a_4$ & $a_3$ & $a_3$ & $a_3$ & $a_3$ \\

      \caption{Reductions using zero-extension and sign-extension of a

        6-bit variable $a=a_5a_4a_3a_2a_1a_0$ to $3$ effective bits.}

    \label{fig:extensions}

  \end{minipage}}

\end{figure}

In contrast to \uclid, we can use the same approach to performing

      \midrule

      CVC4 & & $29$ & $55$ & $32$ & $75$ & & $1\,124$ & $3\,845$ & $2$ & $490$  \\

      Z3 & & $71$ & $93$ & $5$ & $22$ & & $1\,135$ & $4\,162$ & $22$ & $142$ \\

      Q3B & & $\mathbf{94}$ & $\mathbf{94}$ & $0$ & $3$ & & $\mathbf{1\,137}$ & $\mathbf{4\,202}$ & $0$ & $122$  \\

      Q3B & & $\mathbold{94}$ & $\mathbold{94}$ & $0$ & $3$ & & $\mathbold{1\,137}$ & $\mathbold{4\,202}$ & $0$ & $122$  \\

      \bottomrule

    \end{tabularx}

  \end{center}

\end{minipage}}

\end{table}

\begin{figure}[bt]

\begin{figure}

\checkoddpage

\edef\side{\ifoddpage l\else r\fi}

\makebox[\textwidth][\side]{

\end{minipage}}

\end{figure}

Recently, this results was confirmed by the \smt competition 2016 --

our solver is the winner of the quantified-bit vectors category. Table

\ref{tbl:smtcomp} shows official results for this category. The benchmarks

are divided into two groups, with \emph{known} and \emph{unknown}

status. A benchmark has a known status if at least two solvers in the

previous year of the competition agreed whether the benchmark is

satisfiable or unsatisfiable. The results show that Q3B can solve as

many known benchmarks as other solvers, but solves them in the

shortest time. Moreover, Q3B can solve more benchmarks with unknown

status than any of the other solvers.

\begin{table}[bt]

\begin{table}

  \checkoddpage

  \edef\side{\ifoddpage l\else r\fi}

  \makebox[\textwidth][\side]{

      time & &\# solved & avg. CPU time &

      avg. WALL time \\

      \midrule

      Boolector & & $85$ & $1.635$ & & $89$ & $\mathbf{11\,431}$ & $11\,422$ \\

      Boolector & & $85$ & $1.635$ & & $89$ & $\mathbold{11\,431}$ & $11\,422$ \\

      CVC4 & & $85$ & $1.576$ & & $56$ & $29\,464$ & $29\,453$ \\

      Q3B & & $85$ & $\mathbf{0.138}$ & & $\mathbf{99}$ & $12\,111$ & $\mathbf{4\,059}$ \\

      Q3B & & $85$ & $\mathbold{0.138}$ & & $\mathbold{99}$ & $12\,111$ & $\mathbold{4\,059}$ \\

      Z3 & & $85$ & $0.339$ & & $78$ & $16\,721$ & $16\,713$ \\

      \bottomrule

    \end{tabularx}

  \end{minipage}}

\end{table}

Recently, this results was confirmed by the \smt competition 2016 --

our solver is the winner of the quantified-bit vectors category. Table

\ref{tbl:smtcomp} shows official results for this category. The benchmarks

are divided into two groups, with \emph{known} and \emph{unknown}

status. A benchmark has a known status if at least two solvers in the

previous year of the competition agreed whether the benchmark is

satisfiable or unsatisfiable. The results show that Q3B can solve as

many known benchmarks as other solvers, but solves them in the

shortest time. Moreover, Q3B can solve more benchmarks with unknown

status than any of the other solvers.

\section{Other areas of research}

Outside the field of \smt solving, my research also consists in

software verification. In this field, I have co-authored the following

and symbolic execution to allow verification of a real-world

code~\cite{CJSSV16}.

\section{Published papers}

TODO

\begin{itemize}

\item \textsc{Jonáš}, M. and J. \textsc{Strejček}. "\emph{Solving Quantified Bit-Vector

    Formulas Using Binary Decision Diagrams.}" In: Theory and

  Applications of Satisfiability Testing -- SAT 2016 -- 19th

  International Conference, Bordeaux, France, July 5-8, 2016,

  Proceedings. 2016, pp. 267-283

  \smallskip

  I am the main author of the text of the paper. I have also

  implemented the \smt solver and conducted all the experiments.

\item \textsc{Chalupa} M., M. \textsc{Jonáš}, J. \textsc{Slabý}, J. \textsc{Strejček}, and

  M. \textsc{Vitovská}. "\emph{Symbiotic 3: New Slicer and Error-Witness

    Generation -- (Competition Contribution).}" In: Tools and

  Algorithms for the Construction and Analysis of Systems -- 22nd

  International Conference, TACAS 2016, Held as Part of the ETAPS

  2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings,

  pp. 946-949

  \smallskip

  I wrote parts of the paper and prepared the environment that was

  used to run experiments with the implemented tool Symbiotic.

\end{itemize}

%*****************************************