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

Obhajoba/slides.tex

@@ -201,7 +201,13 @@
   \frametitle{Quantified Bit-Vector Logic}
 
   In many software verification applications, quantifiers are
-  necessary.
+  necessary. For example in
+  \begin{itemize}
+  \item invariant generation,
+  \item ranking function synthesis,
+  \item cycle summarization,
+  \item symbolic state equality test.
+  \end{itemize}
 
   \bigskip
 
@@ -211,38 +217,36 @@
 
 \section{Symbolic Approach to Quantified Bit-Vectors}
 \begin{frame}
-  \frametitle{Symbolic Approach to Quantified Bit-Vectors}
-  Bit-vector formulas can be represented by \alert{binary decision diagrams} (BDD).
+  \frametitle{Symbolic Approach to Quantified Bit-Vectors} Boolean and
+  Bit-Vector formulas can be represented by \alert{binary decision
+    diagrams} (BDDs).
 
   \bigskip
 
-  Assuming that $x^{[4]} = x_3x_2x_1x_0$, formula
+  The set of satisfying assignments of a Boolean formula
   \[
-    x^{[4]} >_u 0
+    x \wedge (y \vee \neg z)
   \]
-  is represented by
+  can be represented by a BDD
 
   \begin{center}
   \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 (x) at (2,3) {$x$};
+    \node (y) at (1.1,1.7) {$y$};
+    \node (z) at (2.1,1) {$z$};
 
-    \node [rectangle] (true) at (0,0) {true};
-    \node [rectangle] (false) at (6,0) {false};
+    \node [rectangle] (true) at (0,0) {1};
+    \node [rectangle] (false) at (4,0) {0};
 
     \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);
+    (x) edge [above right] node {} (false)
+    (y) edge [above right] node {} (z)
+    (z) edge [above right] node {} (true);
 
     \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);
+    (x) edge [] node {} (y)
+    (y) edge [] node {} (true)
+    (z) edge [] node {} (false);
 
   \end{tikzpicture}
 \end{center}
@@ -251,18 +255,17 @@
 \begin{frame}
   \frametitle{Symbolic Approach to Quantified Bit-Vectors}
 
-  Efficient algorithm are known for operations with BDDs (conjunction,
+  Efficient algorithm are known for operations with BDDs (e.g. conjunction,
   disjunction, quantifiers).
 
   \bigskip
 
-  Quantification usually reduces the size of the BDD -- useful for
-  quantified bit-vectors.
+  Satisfiability of a BDD can be also easily checked.
 
   \bigskip
 
-  Representation by (reduced and ordered) BDDs is canonical -- formula
-  is unsatisfiable iff the BDD has root false.
+  Quantification usually reduces the size of the BDD -- useful for
+  quantified bit-vectors.
 \end{frame}
 
 \begin{frame}
@@ -330,28 +333,63 @@
 \end{frame}
 
 \begin{frame}
-  \frametitle{Publications}
-  \begin{itemize}
-    \setlength\itemsep{2em}
-  \item \textsc{Mrázek} J., M. \textsc{Jonáš}, V. \textsc{Štill},
-    H. \textsc{Lauko}, and J. \textsc{Barnat}. \emph{``Optimizing and
-      Caching SMT Queries in SymDIVINE (Competition Contribution)''}
-    In: TACAS 2017 (to appear).
+  \frametitle{Reader's questions}
 
-    \bigskip
+  \emph{``Existuje zde předpoklad, že by výzkum v tomto směru (například
+  zvolení konkrétní metody pro uspořádání na základě nějaké analýzy
+  před samotným výpočtem) mohl vést k metodám generující ,,lepší``
+  uspořádání?''}
 
-    Wrote about half of the paper and implemented SMT formula
-    simplifications.
-  \item \textsc{Chalupa} M., M. \textsc{Vitovská}, M. \textsc{Jonáš},
-    J. \textsc{Slabý}, J.~\textsc{Strejček}. \emph{``Symbiotic 4:
-      Beyond Reachability (Competition Contribution)''} In: TACAS 2017
-    (to appear).
+\bigskip
+\bigskip
 
-    \bigskip
+  Ano, takový předpoklad existuje.
+\end{frame}
 
-    Wrote parts of the paper and prepared the environment that was used
-    to run experiments with the implemented tool Symbiotic.
-\end{itemize}
+\begin{frame}
+  \frametitle{Reader's questions}
+
+  \emph{``Má student nějaké konkrétnější představy o metodách zjemňování
+  abstrakcí, které by chtěl implementovat? Budou tyto metody založené
+  na informacích o tvaru/struktuře formule, nebo budou využívat
+  informace z vyšší úrovně, například o verifikovaném programu?''}
+
+\bigskip
+\bigskip
+
+Tyto metody by měly být založené na struktuře formule. Měly by
+využívat informace o důvodu nepřesnosti abstrakce -- například z
+nekorektní model nebo nekorektní nesplnitelné jádro formule.
+\end{frame}
+
+\begin{frame}
+  \frametitle{Reader's questions}
+
+  \emph{``Student má v plánu implementovat extrakci ,,UNSAT core`` pro dočasné
+  BDD vytvořené během výpočtu. K čemu se takové formule dají použít?''}
+
+  \bigskip
+  \bigskip
+
+  Takové formule se dají použít k přesnějšímu určení důvodu
+  nesplnitelnosti formule -- vhodné například pro verifikační nástroje
+  nebo zpřesňování abstrakcí.
+\end{frame}
+
+\begin{frame}
+  \frametitle{Reader's questions}
+
+  \emph{``Co se týká teoretické složitosti problému, z textu mi není jasné,
+  jestli se student bude zaměřovat i na dokázání složitosti třídy
+  AEXPTIME(poly) vzhledem k vlastní inkluzi mezi třídami NEXPTIME a
+  EXPSPACE, nebo zda je cílem ukázat pouze příslušnost problému
+  rozhodování formulí kvantifikovaných bitových vektorů k
+  AEXPTIME(poly).''}
+
+\bigskip
+\bigskip
+
+  V plánu je jen ukázat příslušnost daného problému do třídy AEXPTIME(poly).
 \end{frame}
 
 \end{document}