Merge branch 'master' of https://gitlab.fi.muni.cz/xjonas/DTEDI

Chapters/Chapter01.tex

@@ -8,14 +8,14 @@ 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 of an \smt solver is for a given first-order formula in a
-given first-order theory decide, whether the formula is
+The task for an \smt solver is to decide for a given first-order
+formula in a given first-order theory 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 sub-theories of these theories. From the software analysis and
+and sub-theories of these theories. From the software analysis and0
 verification point of view, a particularly important of these theories
 is the theory of bit-vectors, which can be used to describe properties
 of computer programs, since programs usually use data-types of bounded
@@ -27,8 +27,8 @@ 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.
+integers, the satisfiability of the 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
@@ -39,21 +39,22 @@ lazily translate the formula to the propositional logic
 satisfiability. Therefore, the efficiency of most of the bit-vector
 \smt solvers 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},
+exist: for example 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}, and Z3~\cite{Z3}.
 
-In some cases, quantifier-free formulas are not succint enough and
-quantified formulas are necessary. Quantified bit-vector formulas
-arise naturally for example in applications that need test equality of
-two symbolically represented states, or applicatichch that generate
-loop invariants, ranking functions or loop summaries. 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
+In some cases, quantifier-free formulas are not succinct enough and
+using quantification is necessary keep size of the formula
+reasonable. Bit-vector quantified formulas arise naturally for example
+in applications that need to decide equality of two symbolically
+represented states, or in applications that generate loop invariants,
+ranking functions, or loop summaries. However, the current \smt
+solvers' support of quantified bit-vector logic is much more modest --
+only CVC4, Yices, and Z3 officially support quantifiers in bit-vector
+formulas. Recently, quantifiers have been also implemented in an
+development version of Boolector~\cite{BoolectorComp}. 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.
 
@@ -73,15 +74,16 @@ uninterpreted functions and arrays, which 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 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 concerning
-the computational complexity of bit-vector
+summarizes the state of the art and is divided into six
+sections. Section~\ref{sec:prelim} introduces necessary background and
+notations from propositional logic and first-order
+logic. Section~\ref{sec:sat} describes approaches to solving
+propositional satisfiability and Section~\ref{sec:smt} describes
+approaches to solving satisfiability modulo theories. Sections
+\ref{sec:qfbv} and \ref{sec:bv} are devoted to solving quantifier-free
+and quantified formulas over the theory of bit-vectors,
+respectively. Finally, Section~\ref{sec:complexity} section describes
+results concerning 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

Chapters/Chapter02.tex

@@ -3,6 +3,7 @@
 %*****************************************
 
 \section{Preliminaries}
+\label{sec:prelim}
 
 This section introduces the notation used in the rest of this
 chapter. The exposition of the propositional logic is mainly based on
@@ -146,50 +147,6 @@ $\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
-% Enderton~\cite{End01}.
-
-% Definitions for the first-order quantifier-free formulas are similar
-% to those from subsection \ref{prelim:prop}, except that the set $\P$
-% now contains a fixed finite set of first-order atoms that do not
-% contain free variables. For example, if we consider a set of atoms
-% $\P = \{ x \geq y + 1, x = 4 \}$, where $x, y, 1$, and $4$ are
-% constant symbols, $x \geq y + 1~\vee~\neg (x = 4)$ is a clause.
-
-% A \emph{theory} $\mathcal{T}$ is a set of first-order structures.  A formula
-% $\varphi$ is $\mathcal{T}$-\emph{satisfiable} or $\mathcal{T}$-\emph{consistent} if there
-% is a structure $M \in T$ in which the formula $F$ holds in the
-% standard first-order sense. The formula $\varphi$ is
-% $\mathcal{T}$-\emph{unsatisfiable} or $\mathcal{T}$-\emph{inconsistent} otherwise. If the
-% distinction is necessary, we call literals over a specific background
-% theory $\mathcal{T}$-literals. 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}.
-
-% Using the same notation as in the propositional logic, a partial
-% assignment is a set of literals and can be therefore seen as a
-% conjunction of literals, i.e. a formula. If a partial assignment $M$
-% is a propositional model of a given formula $\varphi$ and the partial
-% assignment $M$ is $\mathcal{T}$-consistent, we say that $M$ is a
-% $\mathcal{T}$-\emph{model} of $\varphi$. If $\varphi$ and $\psi$ are formulas
-% such that $\varphi \wedge \neg \psi$ is $\mathcal{T}$-inconsistent, we say that
-% \emph{$\varphi$ entails $\psi$ in $\mathcal{T}$} and write it as
-% $\varphi \models_T \psi$.
-
-% \subsection{First-order quantified formulas}
-% As the first-order formulas containing quantifiers are concerned, we
-% impose no restrictions on their form. We again suppose the knowledge
-% and definitions from the standard first-order logic and model theory.
-
-% A first-order formula $\varphi$ is in a \emph{negation normal form},
-% if the only logical connectives in $\varphi$ are negations,
-% conjunctions, and disjunctions and all negations in $\varphi$ occur in
-% front of a literal. Every first-order formula can be transformed to a
-% formula without existential quantifiers by introducing uninterpreted
-% functions; this process is known as \emph{Skolemization}.
-
 \subsection{Many-sorted logic}
 
 For some theories, it can be convinient to distinguish several types
@@ -225,6 +182,7 @@ entailment, and so on are also straightforward and can also be found
 in Enderton~\cite{End01}.
 
 \section{Propositional satisfiability}
+\label{sec:sat}
 
 A \emph{propositional satisfiability problem} (\sat) is, for a given
 formula $\varphi$ in \cnf, to decide whether it is satisfiable. The
@@ -245,7 +203,7 @@ the other hand, if after elimination of all variables no clauses
 remain, the formula is satisfiable. The main problem of \dppr is its
 space complexity, since the number of the clauses may grow
 exponentially even for simple formulas. To alleviate this problem, the
-refinement of \dppr algorithm was introduced in 1962 by Davis, Putnam,
+refinement of \dppr algorithm was introduced in 1962 by Davis,
 Logemann and Loveland~\cite{DPLL62}.
 
 The Davis--Putnam--Logemann--Loveland \quotegraffito{If you don't know
@@ -377,6 +335,7 @@ recently used to solve a long-standing open problem in the Ramsey
 theory~\cite{HKM16}.
 
 \section{Satisfiability modulo theories}
+\label{sec:smt}
 
 Similarly to \sat, the \emph{satisfiability modulo theories problem}
 (\smt) is to decide for a given a \cnf formula $\varphi$ in a fixed
@@ -764,6 +723,7 @@ the theory of integers, the function $f(x) = k \times x$ is invertible
 in bit-vectors precisely if $k$ is odd.
 
 \section{Satisfiability of quantified bit-vector formulas}
+\label{sec:bv}
 
 Although the bit-vector theory admits quantifier elimination by
 expanding all quantifiers with all possible bit-vector values of the

Chapters/ChapterA2.tex

@@ -13,14 +13,16 @@ July 2016, Bordeaux, France.
 \item TACAS 2016, April 2016, Eindhoven, The Netherlands
 \end{itemize}
 \section{Teaching}
-I have tutored seminar groups for the following courses:
+At my faculty, I have tutored seminar groups for the following
+courses:
 \begin{itemize}
 \item Automata, Grammars, and Complexity (2014--now)
 \item Formal Languages and Automata (2016--now)
 \item Non-Imperative Programming (2015--now)
 \end{itemize}
 \smallskip
-\noindent I have also been a reader of the following bachelor theses:
+\noindent I have also been an official reader of the following
+bachelor theses:
 \begin{itemize}
 \item Jan Mrázek -- Caching SMT Queries in SymDivine
 \item Jakub Lédl -- Many-sorted equational logic