Skip to content
Snippets Groups Projects
Commit cc7d22bb authored by Martin Jonas's avatar Martin Jonas
Browse files

Small changes

parent e2016e8c
No related branches found
No related tags found
No related merge requests found
...@@ -956,7 +956,8 @@ year = {2005}, ...@@ -956,7 +956,8 @@ year = {2005},
of Systems - 22nd International Conference, {TACAS} of Systems - 22nd International Conference, {TACAS}
2016, Held as Part of the ETAPS 2016, Eindhoven, The 2016, Held as Part of the ETAPS 2016, Eindhoven, The
Netherlands, April 2-8, 2016, Proceedings}, Netherlands, April 2-8, 2016, Proceedings},
pages = {946--949} pages = {946--949},
year = {2016}
} }
@inproceedings{JS16, @inproceedings{JS16,
...@@ -1338,3 +1339,13 @@ pages={358--372}, ...@@ -1338,3 +1339,13 @@ pages={358--372},
volume = {8044}, volume = {8044},
publisher = {Springer} publisher = {Springer}
} }
@inproceedings{Lei10,
author = {K. Rustan M. Leino},
title = {Dafny: An Automatic Program Verifier for Functional Correctness},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 16th
International Conference, LPAR-16, Dakar, Senegal, April 25-May 1,
2010, Revised Selected Papers},
pages = {348--370},
year = {2010}
}
...@@ -15,13 +15,13 @@ also has the ability to provide its model. Modern \smt solvers support ...@@ -15,13 +15,13 @@ 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, of integers, real numbers, floating-point numbers, arrays, strings,
inductively defined data types, bit-vectors, and various combinations inductively defined data types, bit-vectors, and various combinations
and sub-theories of these theories~\cite{BFT15, ZZG13, RB16}. From the and fragments of formulas over these theories~\cite{BFT15, ZZG13,
software analysis and verification point of view, a particularly RB16}. From the software analysis and verification point of view, a
important of these theories is the theory of bit-vectors, which can be particularly important of these theories is the theory of bit-vectors,
used to describe properties of computer programs, since programs which can be used to describe properties of computer programs, since
usually use data-types of bounded size instead of mathematical programs usually use data-types of bounded size instead of
integers. Additionally, operations over these bounded data-types mathematical integers. Additionally, operations over these bounded
naturally corespond to operations of the bit-vector theory. data-types naturally correspond to operations of the bit-vector theory.
The benefit of describing properties of programs by bit-vector The benefit of describing properties of programs by bit-vector
formulas is twofold. Formulas in the bit-vector theory allow to model formulas is twofold. Formulas in the bit-vector theory allow to model
...@@ -33,27 +33,27 @@ even if the multiplication is allowed. ...@@ -33,27 +33,27 @@ even if the multiplication is allowed.
Therefore, quantifier-free bit-vector formulas are used in tools for Therefore, quantifier-free bit-vector formulas are used in tools for
symbolic execution, bounded model checking, analysis of hardware symbolic execution, bounded model checking, analysis of hardware
circuits, static analysis, or test generation~\cite{CGPD08, CDE08, circuits, static analysis, or test generation~\cite{CGPD08, CDE08,
CFM12}. Most of the current \smt solvers for the quantifier-free Lei10, CFM12}. Most of the current \smt solvers for the
bit-vector formulas eagerly or lazily translate the formula to the quantifier-free bit-vector formulas eagerly or lazily translate the
propositional logic (\emph{bit-blasting}) and use an efficient \sat formula to the propositional logic (\emph{bit-blasting}) and use an
solver to decide its satisfiability. Therefore, the efficiency of most efficient \sat solver to decide its satisfiability. Therefore, the
of the bit-vector \smt solvers is tightly connected to the efficiency efficiency of most of the bit-vector \smt solvers is tightly connected
of the \sat solvers. Plenty of solvers for the quantifier-free to the efficiency of the \sat solvers. Plenty of solvers supporting
bit-vector formulas exist: Beaver~\cite{Beaver}, the quantifier-free bit-vector formulas exist: Beaver~\cite{Beaver},
Boolector~\cite{Boolector}, CVC4~\cite{CVC4}, MathSAT5~\cite{MathSAT}, Boolector~\cite{Boolector}, CVC4~\cite{CVC4}, MathSAT5~\cite{MathSAT},
OpenSMT~\cite{OpenSMT}, Sonolar~\cite{Sonolar}, Spear~\cite{Spear}, OpenSMT~\cite{OpenSMT}, Sonolar~\cite{Sonolar}, Spear~\cite{Spear},
STP~\cite{STP}, UCLID~\cite{LS04}, Yices~\cite{Yices}, and STP~\cite{STP}, UCLID~\cite{LS04}, Yices~\cite{Yices}, and
Z3~\cite{Z3}. Z3~\cite{Z3}.
In some cases, quantifier-free formulas are not succinct enough and In some cases, quantifier-free formulas are not succinct enough and
using quantification is necessary keep size of the formula using quantification is necessary to keep the size of the formula
reasonable. Bit-vector quantified formulas arise naturally for example reasonable. Quantified bit-vector formulas arise naturally for example
in applications that need to decide equality of two symbolically in applications that need to decide equality of two symbolically
represented states~\cite{BHB14}, or in applications that generate loop represented states~\cite{BHB14}, or in applications that generate loop
invariants, ranking functions, or loop invariants, ranking functions, or loop
summaries~\cite{WHD13,KLW13}. However, the current \smt solvers' summaries~\cite{WHD13,KLW13}. However, the current \smt solvers'
support of quantified bit-vector logic is much more modest -- only support of quantified bit-vector logic is modest -- only CVC4, Yices,
CVC4, Yices, and Z3 officially support quantifiers in bit-vector and Z3 officially support quantifiers in bit-vector
formulas. Recently, quantifiers have been also implemented in an formulas. Recently, quantifiers have been also implemented in an
development version of Boolector~\cite{BoolectorComp}. All of these development version of Boolector~\cite{BoolectorComp}. All of these
\smt solvers solve quantified bit-vector formulas by some variant of \smt solvers solve quantified bit-vector formulas by some variant of
...@@ -61,8 +61,8 @@ quantifier-instantiation and using a solver for quantifier-free ...@@ -61,8 +61,8 @@ quantifier-instantiation and using a solver for quantifier-free
formulas as an oracle. formulas as an oracle.
In the last year, we have proposed a different approach. We have In the last year, we have proposed a different approach. We have
implemented a symbolic solver Q3B, which is based on binary decision implemented a symbolic \smt solver Q3B, which is based on binary
diagrams, and have shown that it can not only compete with decision diagrams. We have shown that it can not only compete with
state-of-the art \smt solvers, but outperforms them in many state-of-the art \smt solvers, but outperforms them in many
cases~\cite{JS16}. However, \bdds are not a silver bullet; the cases~\cite{JS16}. However, \bdds are not a silver bullet; the
symbolic \smt solver fails on formulas containing non-trivial symbolic \smt solver fails on formulas containing non-trivial
...@@ -71,14 +71,14 @@ study, I plan to develop a hybrid approach to solving quantified ...@@ -71,14 +71,14 @@ study, I plan to develop a hybrid approach to solving quantified
bit-vectors, which combines symbolic representation by \bdds with bit-vectors, which combines symbolic representation by \bdds with
search techniques employed by existing state-of-the-art solvers. I search techniques employed by existing state-of-the-art solvers. I
also plan to continue developing the symbolic solver Q3B itself, also plan to continue developing the symbolic solver Q3B itself,
namely improving its efficiency and adding support for features as namely improve its efficiency and add support for features as
uninterpreted functions and arrays, which are important in the software uninterpreted functions and arrays, which are important in the
verification. software verification.
The thesis proposal is organized as follows. Chapter~\ref{ch:sota} The thesis proposal is organized as follows. Chapter~\ref{ch:sota}
summarizes the state of the art and is divided into six summarizes the state of the art and is divided into six
sections. Section~\ref{sec:prelim} introduces necessary background and sections. Section~\ref{sec:prelim} introduces necessary background and
notations from propositional logic and first-order notations from the propositional and first-order
logic. Section~\ref{sec:sat} describes approaches to solving logic. Section~\ref{sec:sat} describes approaches to solving
propositional satisfiability and Section~\ref{sec:smt} describes propositional satisfiability and Section~\ref{sec:smt} describes
approaches to solving satisfiability modulo theories. Sections approaches to solving satisfiability modulo theories. Sections
...@@ -86,7 +86,7 @@ approaches to solving satisfiability modulo theories. Sections ...@@ -86,7 +86,7 @@ approaches to solving satisfiability modulo theories. Sections
and quantified formulas over the theory of bit-vectors, and quantified formulas over the theory of bit-vectors,
respectively. Finally, Section~\ref{sec:complexity} section describes respectively. Finally, Section~\ref{sec:complexity} section describes
results concerning the computational complexity of bit-vector results concerning the computational complexity of bit-vector
logics. Chapter~\ref{ch:achieved} describes results, which we have logics. Chapter~\ref{ch:achieved} describes results that we have
achieved during the first two years of my PhD achieved during the first two years of my PhD
study. Chapter~\ref{ch:aims} presents the aim of the thesis and states study. Chapter~\ref{ch:aims} presents the aim of the thesis and states
plans for the remaining part of my PhD study. plans for the remaining part of my PhD study.
......
...@@ -150,7 +150,7 @@ $\mathcal{T}$- prefixes. ...@@ -150,7 +150,7 @@ $\mathcal{T}$- prefixes.
\subsection{Many-sorted logic} \subsection{Many-sorted logic}
For some theories, it can be convinient to distinguish several types For some theories, it can be convenient to distinguish several types
of objects instead of having only one universe. This can be achieved of objects instead of having only one universe. This can be achieved
by using a \emph{many-sorted logic}. In contrast with a single-sorted by using a \emph{many-sorted logic}. In contrast with a single-sorted
signature, defined in the previous subsection, a \emph{many-sorted signature, defined in the previous subsection, a \emph{many-sorted
...@@ -168,7 +168,7 @@ Enderton~\cite{End01}. ...@@ -168,7 +168,7 @@ Enderton~\cite{End01}.
For a many-sorted signature $\Sigma$, a \emph{$\Sigma$-structure} For a many-sorted signature $\Sigma$, a \emph{$\Sigma$-structure}
$\mathcal{A}$ consists of an assignment $(\_)^\mathcal{A}$, which to $\mathcal{A}$ consists of an assignment $(\_)^\mathcal{A}$, which to
each sort symbol $S \in \Sigma^S$ assigns a non-empty set each sort symbol $S \in \Sigma^S$ assigns a non-empty set
$S^\mathcal{A}$, caled the \emph{domain of S in $\mathcal{A}$}, to $S^\mathcal{A}$, called the \emph{domain of S in $\mathcal{A}$}, to
each variable $x$ of sort $S$ assigns an element each variable $x$ of sort $S$ assigns an element
$x^\mathcal{A} \in S^\mathcal{A}$, to each function symbol $x^\mathcal{A} \in S^\mathcal{A}$, to each function symbol
$f \in \Sigma^f$ of an arity $(S_1, \ldots, S_n, S_{n+1})$ assigns a $f \in \Sigma^f$ of an arity $(S_1, \ldots, S_n, S_{n+1})$ assigns a
...@@ -380,7 +380,7 @@ For a detailed description of these theories and implementation of the ...@@ -380,7 +380,7 @@ For a detailed description of these theories and implementation of the
respective $\mathcal{T}$-solvers, we refer the reader for example to the book of respective $\mathcal{T}$-solvers, we refer the reader for example to the book of
Bradley and Manna~\cite{BM07}. Bradley and Manna~\cite{BM07}.
In pracitce, a satisfiability of formulas using a combination of In practice, a satisfiability of formulas using a combination of
theories is often needed. For example, a single formula may be using theories is often needed. For example, a single formula may be using
integers, arrays, and uninterpreted functions. In their seminal work, integers, arrays, and uninterpreted functions. In their seminal work,
Nelson and Oppen have shown that satisfiability of combination of Nelson and Oppen have shown that satisfiability of combination of
......
...@@ -57,12 +57,12 @@ the size of the formula. Dually, the existential quantification can be ...@@ -57,12 +57,12 @@ the size of the formula. Dually, the existential quantification can be
distributed over disjunctions. distributed over disjunctions.
Moreover, universal quantification can distribute over disjunctions in Moreover, universal quantification can distribute over disjunctions in
cases where the variable bound by the quantifier does not occurg in one cases where the variable bound by the quantifier does not occur in one
of the disjuncts. This leads to the following rule and its dual of the disjuncts. This leads to the following rule and its dual
version, which is known as \emph{miniscoping}~\cite{Har09}: version, which is known as \emph{miniscoping}~\cite{Har09}:
\[ \[
\forall x. \, (\varphi ~\vee~ \psi)~~\leadsto~~(\forall x . \, \forall x. \, (\varphi[x] ~\vee~ \psi)~~\leadsto~~(\forall x . \,
\varphi) ~\vee~ \psi, \varphi[x]) ~\vee~ \psi,
\] \]
where $x$ does not occur freely in $\psi$. Note that the scope of the where $x$ does not occur freely in $\psi$. Note that the scope of the
quantifier is again reduced, which can lead to smaller intermediate quantifier is again reduced, which can lead to smaller intermediate
...@@ -218,10 +218,15 @@ which uses quantified formulas to decide the equality of two symbolic ...@@ -218,10 +218,15 @@ which uses quantified formulas to decide the equality of two symbolic
states. On this set of benchmarks, our solver Q3B also has better states. On this set of benchmarks, our solver Q3B also has better
performance than \smt solvers based on the quantifier instantiation performance than \smt solvers based on the quantifier instantiation
and bit-blasting. Table \ref{tbl:results} shows the numbers of and bit-blasting. Table \ref{tbl:results} shows the numbers of
formulas solved by each solver and figure \ref{fig:quantilePlots} formulas solved by each solver and Figure \ref{fig:quantilePlots}
presents the quantile plot of CPU times needed to solve these presents the quantile plot of CPU times needed to solve these
formulas. formulas.
All experiments were performed on a Debian machine with two six-core
Intel Xeon E5-2620 2.00GHz processors and 128 GB of RAM. Each
benchmark run was limited to use 3 processor cores, 4 GB of RAM and 20
minutes of CPU time (if not stated otherwise).
\begin{table} \begin{table}
\checkoddpage \checkoddpage
\edef\side{\ifoddpage l\else r\fi} \edef\side{\ifoddpage l\else r\fi}
...@@ -298,8 +303,9 @@ formulas. ...@@ -298,8 +303,9 @@ formulas.
\end{minipage}} \end{minipage}}
\end{table} \end{table}
Recently, these results were confirmed by the \smt competition 2016 -- Recently, these results were confirmed by the \smt competition
our solver is the winner of the quantified-bit vectors category. Table 2016\footnote{\url{http://smtcomp.sourceforge.net/2016/}} -- our
solver is the winner of the quantified-bit vectors category. Table
\ref{tbl:smtcomp} shows official results for this category. The \ref{tbl:smtcomp} shows official results for this category. The
benchmarks are divided into two groups, with \emph{known} and benchmarks are divided into two groups, with \emph{known} and
\emph{unknown} status. A benchmark has a known status if at least two \emph{unknown} status. A benchmark has a known status if at least two
......
...@@ -5,13 +5,13 @@ ...@@ -5,13 +5,13 @@
\section{Objectives and Expected Results} \section{Objectives and Expected Results}
\subsection{Symbolic solver for quantified bit-vectors} \subsection{Symbolic solver for quantified bit-vectors}
I plan to continue developing the implemented symbolic \smt solver Throughout the rest of my PhD study, I plan to continue developing the
Q3B, which is aimed at solving quantified bit-vector formulas. In implemented symbolic \smt solver Q3B, which is aimed at solving
particular, I plan to add support for uninterpreted functions and the quantified bit-vector formulas. In particular, I plan to add support
theory of arrays, which is highly desirable for applications in the for uninterpreted functions and the theory of arrays, which is highly
program verification. I also want to implement extraction of an desirable for applications in the program verification. I also want to
unsatisfiable core from the intermediate \bdds that were produced implement extraction of an unsatisfiable core from the intermediate
during the computation. \bdds that were produced during the computation.
Additionally, currently implemented approximations are very simple and Additionally, currently implemented approximations are very simple and
could benefit from better refinement in the case that the current could benefit from better refinement in the case that the current
...@@ -61,7 +61,7 @@ correctness is not yet complete. ...@@ -61,7 +61,7 @@ correctness is not yet complete.
Moreover, the simplifications of formulas with unconstrained variables Moreover, the simplifications of formulas with unconstrained variables
can be further extended. For example, if a formula contains a term can be further extended. For example, if a formula contains a term
$k \times x$ in which the variable $x$ is unconstrained, this term can $k \times x$ in which the variable $x$ is unconstrained, this term can
be replaced by a simpler term regargless the parity of the value be replaced by a simpler term regardless the parity of the value
$k$. In particular, if $i$ is the largest number for which $2^i$ $k$. In particular, if $i$ is the largest number for which $2^i$
divides the constant $k$ and the unconstrained variable $x$ has divides the constant $k$ and the unconstrained variable $x$ has
bit-width $n$, the term $k \times x$ can be rewritten to bit-width $n$, the term $k \times x$ can be rewritten to
...@@ -87,18 +87,20 @@ those complexity classes. We are working on a proof which shows that ...@@ -87,18 +87,20 @@ those complexity classes. We are working on a proof which shows that
BV2 is complete for the class of problems solvable by the BV2 is complete for the class of problems solvable by the
\emph{alternating Turing machine} (\atm) with the exponential space \emph{alternating Turing machine} (\atm) with the exponential space
and \emph{polynomial number of alternations} with respect to log-space and \emph{polynomial number of alternations} with respect to log-space
reduction. This class is usually denoted as \AEXPTIMEp and is known to reductions. This class is usually denoted as \AEXPTIMEp and is known
be in between \NEXPTIME and \EXPSPACE~\cite{HKVV15, Luc16}. However, to be in between \NEXPTIME and \EXPSPACE~\cite{HKVV15,
whether any of the inclusions is proper is not known. Luc16}. However, whether any of the inclusions is proper is not
known.
\section{Progression Schedule} \section{Progression Schedule}
The plan of my future study and research activities is following: The plan of my future study and research activities is following:
\begin{description}[style=nextline,leftmargin=0.8cm] \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 maintaining of the \item [now -- January 2019] Improvements and maintaining of the
developed symbolic \smt solver Q3B. developed symbolic \smt solver Q3B.
\item [now -- January 2017] Extending unconstrained variable
propagation to quantified formulas and to non-linear multiplication
and division.
\item [January 2017] Doctoral exam and defense of this thesis proposal. \item [January 2017] Doctoral exam and defense of this thesis proposal.
\item [February 2017 -- April 2017] Proving a precise complexity class \item [February 2017 -- April 2017] Proving a precise complexity class
of the quantified bit-vector formulas without uninterpreted functions of the quantified bit-vector formulas without uninterpreted functions
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment