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

First version of defense

parent dd110059
%balíček na A4
......@@ -13,7 +13,7 @@
......@@ -28,6 +28,18 @@
visible on/.style={alt=#1{}{invisible}},
red on/.style={alt={#1{fill=red!10}{blank}}},
alt/.code args={<#1>#2#3}{%
\alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path
......@@ -111,9 +123,261 @@
\section{Propositional Satisfiability}
\frametitle{Propositional Satisfiability}
Propositional satisfiability problem (SAT) -- decide whether a
propositional formula is satisfiable.
For example
$\varphi = (y \vee z)~\wedge~(\neg y \vee z)~\wedge~(y \vee x
\vee z)~\wedge~(y \vee \neg x \vee \neg z)$ is satisfiable.
Usually solved by a \alert{conflict driven clause learning} algorithm (CDCL), which relies on:
\item preprocessing,
\item variable assignment (with heuristics),
\item unit propagation,
\item conflict analysis,
\item clause learning,
\item backtracking,
\item restarts.
% \begin{example}
% $\varphi = (\neg y \vee z)~\wedge~(\neg y \vee z)~\wedge~(y \vee x \vee z)~\wedge~(y \vee \neg x \vee \neg z)$.
% \bigskip
% \begin{tikzpicture}[every node/.style={draw}]
% \node (e) at (5,4) {decide};
% \node [visible on=<2->] (x) at (2,3) {decide};
% \node [visible on=<3->] (xy) at (0,2) {propagate};
% \node [visible on=<4->] (xyz) at (0,0.5) {conflict (learn $\neg y$)};
% \node [visible on=<5->] (-y) at (9,3) {decide};
% \node [visible on=<6->] (-yz) at (7,2) {propagate};
% \node [visible on=<7->] (-yz-x) at (7,0.5) {sat};
% \path[auto, every node/.style={}, above]
% (e) edge [visible on=<2->] node {$x$} (x)
% (x) edge [visible on=<3->] node {$y$} (xy)
% (xy) edge [visible on=<4->, left] node {$z$} (xyz)
% (e) edge [visible on=<5->] node {$\neg y$} (-y)
% (-y) edge [visible on=<6->] node {$z$} (-yz)
% (-yz) edge [visible on=<7->, left] node {$\neg x$} (-yz-x);
% \end{tikzpicture}
% \end{example}
\section{Satisfiability Modulo Theories}
\frametitle{Satisfiability Modulo Theories}
Decide the satisfiability of a first-order formula in a given
Function symbols are given interpretations by the theory.
Traditionally solved by the \alert{CDCL modulo theories} -- combination of
CDCL and a specialized theory solver.
Let $\varphi = (x + y = 3) \wedge (x > 1) \wedge (y = 2 \vee y = 1)$.
\item Propositional model $\{ x + y = 3,~x > 1,~y = 2 \} $.
\item This model \textbf{is not} consistent with the theory of integers.
\item Conjoin $\neg (x + y = 3) \vee \neg (x > 1) \vee \neg (y = 2)$ to $\varphi$.
\item Propositional model $\{ x + y = 3,~x > 1,~y = 1 \} $.
\item This model \textbf{is} consistent with the theory of integers.
\item $\varphi$ is satisfiable.
\section{Theory of Bit-Vectors}
\frametitle{Theory of Bit-Vectors}
Theory of bit-vectors describes bounded integers (or vectors of
bits) with:
\item arithmetic operations,
\item bitwise operations,
\item comparison.
Often used in modelling of software.
Different from mathematical integers -- for example the formula
\varphi = (x^{[32]} >_s 0)~\wedge~(y^{[32]} >_s 0)~\wedge~(x^{[32]} + y^{[32]} = 0)
is \alert{satisfiable}.
\section{Quantifier-free Bit-Vector Logic}
\frametitle{Quantifier-free Bit-Vector Logic} Quantifier-free
bit-vector formulas usually solved by reduction to a propositional
formula (\emph{bit-blasting}) and using a SAT solver.
Approach taken by Z3, CVC4, Boolector, UCLID, Yices, \ldots.
Alternative approaches exist:
\item model-constructing satisfiability calculus,
\item abstract CDCL,
\item stochastic local search.
\section{Quantified Bit-Vector Logic}
\frametitle{Quantified Bit-Vector Logic}
In many software verification applications, quantifiers are
Quantifier bit-vector formulas traditionally solved by
\alert{quantifier instantiation}.
Let $\varphi = 3 < a ~\wedge~ \forall x\,(a \not = 2 \times x)$
\item $3 < a$ is satisfiable with model $a = 4$.
\item $a = 4$ not a model of $\forall x \,(a \not = 2 \times x)$ (corresponding counter-example is $x = 2$).
\item Add instance of the quantifier for $x = 2$.
\item $3 < a ~\wedge~ (a \not = 2 \times 2)$ is satisfiable with model $a = 5$.
\item $a = 5$ is a model of $\forall x \,(a \not = 2 \times x)$.
\item $\varphi$ is satisfiable
\section{Symbolic Approach to Quantified Bit-Vectors}
\frametitle{Symbolic Approach to Quantified Bit-Vectors}
Bit-vector formulas can be represented by \alert{binary decision diagrams} (BDD).
Assuming that $x^{[4]} = x_3x_2x_1x_0$, formula
x^{[4]} >_u 0
is represented by
\begin{tikzpicture}[every node/.style={draw, circle}]
\node (x0) at (2,4) {$x_0$};
\node (x1) at (3,3) {$x_1$};
\node (x2) at (4,2) {$x_2$};
\node (x3) at (5,1) {$x_3$};
\node [rectangle] (true) at (0,0) {true};
\node [rectangle] (false) at (6,0) {false};
\path[auto, every node/.style={}, above, dashed]
(x0) edge [above right] node {$0$} (x1)
(x1) edge [above right] node {$0$} (x2)
(x2) edge [above right] node {$0$} (x3)
(x3) edge [above right] node {$0$} (false);
\path[auto, every node/.style={}, above left]
(x0) edge [] node {$1$} (true)
(x1) edge [] node {$1$} (true)
(x2) edge [] node {$1$} (true)
(x3) edge [] node {$1$} (true);
\frametitle{Symbolic Approach to Quantified Bit-Vectors}
Efficient algorithm are known for operations with BDDs (conjunction,
disjunction, quantifiers).
Quantification usually reduces the size of the BDD -- useful for
quantified bit-vectors.
We have implemented the solver Q3B, which
\item simplifies the formula,
\item converts the formula to the BDD,
\item tries to use approximations if the precise BDD computation is
too expensive.
Results show that Q3B is \alert{more efficient} than standard SMT solvers.
\section{Aims of the Work}
\frametitle{Aims of the Work}
\textbf{Major aims}
\item Further development of the symbolic solver for quantified-bit
\item Hybrid approach to quantified bit-vectors.
\textbf{Minor aims}
\item Determining a computational complexity of quantified bit-vector logic with
bit-widths represented in binary.
\item Extending simplifications using unconstrained variables
\item \textsc{Jonáš}, M. and J. \textsc{Strejček}. \emph{``Solving
Quantified Bit-Vector Formulas Using Binary Decision Diagrams.''}
In: SAT 2016, Bordeaux, France, July 5-8, 2016, Proceedings. 2016,
pp. 267-283 \bigskip
Main author of the text of the paper, 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: TACAS 2016, Eindhoven, The Netherlands, April
2-8, 2016, Proceedings, pp. 946-949
Wrote parts of the paper and prepared the environment that was used
to run experiments with the implemented tool Symbiotic.
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