Commit 5663862f by Martin Jonas

### A few changes.

parent beacfd2d
 ... ... @@ -202,7 +202,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 ... ... @@ -212,38 +218,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} ... ... @@ -252,18 +256,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} ... ... @@ -326,6 +329,66 @@ \end{itemize} \end{frame} \begin{frame} \frametitle{Reader's questions} \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í?''} \bigskip \bigskip Ano, takový předpoklad existuje. \end{frame} \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} %%% Local Variables: ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!