Commit 6a27c39d authored by Martin Jonas's avatar Martin Jonas
Browse files

Small changes

parent 99f3d906
......@@ -2,26 +2,26 @@
\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.
During the last decades, the area \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
The task of 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
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
inductively defined data types, bit-vectors, and various combinations
and sub-theories 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.
is the theory of bit-vectors, which can be used to describe properties
of computer programs, since programs usually use data-types of bounded
size instead of mathematical integers. Additionally, operations over
these bounded data-types naturally corespond to operations of the
bit-vector theory.
The benefit of describing properties of programs by bit-vector
formulas is twofold. Formulas in the bit-vector theory allow to model
......@@ -36,25 +36,26 @@ 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
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},
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}.
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. 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.
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
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
......@@ -68,23 +69,23 @@ 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
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 problem
and the third section describes approaches to solving satisfiability
modulo theories. The fourth and fifth sections are devoted to solving
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 about the
computational complexity of bit-vector
respectively. The final, sixth, 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
plans remaining part of the PhD study.
plans for the remaining part of my PhD study.
%%% Local Variables:
%%% mode: latex
......
......@@ -23,7 +23,7 @@
\vfill
\mySubtitle \\
\spacedlowsmallcaps{\mySubtitle} \\
%\myDegree \\
%\myDepartment \\
\smallskip
......@@ -33,7 +33,9 @@
\vfill
\end{center}
\noindent \myFaculty, \myUni \\
\noindent Supervisor: \myProf
\begin{tabularx}{\linewidth}{l X r}
\myFaculty & & \spacedlowsmallcaps{Supervisor} \\
\myUni & & \myProf
\end{tabularx}
\end{addmargin}
\end{titlepage}
......@@ -42,7 +42,7 @@
% ****************************************************************************************************
% 2. Personal data and user ad-hoc commands
% ****************************************************************************************************
\newcommand{\myTitle}{SMT Solving Bit-Vector Formulas\xspace}
\newcommand{\myTitle}{SMT Solving for the Theory of Bit-Vectors\xspace}
\newcommand{\mySubtitle}{PhD Thesis Proposal\xspace}
%\newcommand{\myDegree}{Doktor-Ingenieur (Dr.-Ing.)\xspace}
\newcommand{\myName}{Martin Jonáš\xspace}
......
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