Commit 2f52fea4 by Martin Jonáš

### Small changes.

parent beacfd2d
 ... ... @@ -144,10 +144,10 @@ For example \begin{itemize} \item $x + y = 3~\wedge~x > 1~\wedge~y > x$ is satisfiable over the \item $x + y = 3~\wedge~x > 1~\wedge~y > x$ is \alert{satisfiable} over the integers, \item $3 = x + x$ is unsatisfiable over the integers, \item $3 = x + x$ is satisfiable over the rationals. \item $3 = x + x$ is \alert{unsatisfiable} over the integers, \item $3 = x + x$ is \alert{satisfiable} over the rationals. \end{itemize} \end{frame} ... ... @@ -164,22 +164,21 @@ \] should be satisfiable due to overflows. Theory of bit-vectors describes bounded integers (or vectors of \bigskip \pause The \alert{theory of bit-vectors} describes bounded integers (or vectors of bits) with: \begin{itemize} \item arithmetic operations, \item bitwise operations, \item comparison. \end{itemize} \smallskip Often used in modelling of software. \end{frame} \section{Quantifier-free Bit-Vector Logic} \section{Quantifier-Free Bit-Vector Logic} \begin{frame} \frametitle{Quantifier-free Bit-Vector Logic} Quantifier-free \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. ... ... @@ -285,7 +284,7 @@ \section{Aims of the Work} \begin{frame} \frametitle{Aims of the Work} \textbf{Major aims} \textcolor{main}{\textbf{Major aims}} \begin{itemize} \item Further development of the symbolic solver for quantified-bit vectors. ... ... @@ -294,7 +293,7 @@ \bigskip \textbf{Minor aims} \textcolor{main}{\textbf{Minor aims}} \begin{itemize} \item Determining a computational complexity of quantified bit-vector logic with bit-widths represented in binary. ... ... @@ -307,12 +306,16 @@ \begin{frame} \frametitle{Publications} \begin{itemize} \setlength\itemsep{2em} \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 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. 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 ... ... @@ -326,6 +329,31 @@ \end{itemize} \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). \bigskip 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 Wrote parts of the paper and prepared the environment that was used to run experiments with the implemented tool Symbiotic. \end{itemize} \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!