Loading Chapters/Chapter03.tex +18 −0 Original line number Diff line number Diff line Loading @@ -6,7 +6,25 @@ \section{Expected Outputs} \newpage \section{Progression Schedule} The plan of my future study and research activities is following: \begin{description}[style=nextline,leftmargin=0.8cm] \item [now -- January 2017] Extension of unconstrained variable propagation to quantified formulas and to non-linear multiplication. \item [January 2017] Doctoral exam and defence of this thesis proposal. \item [January 2017 -- May 2017] Complexity of the quantfied bit-vector formulas without uninterpreted functions and with binary encoded bit-widths. \item [May 2017 -- January 2018] Development of the hybrid approach to \smt solving of quantified bit-vector formulas combining symbolic representation of formulas with \dpllt or \mcsat. \item [January 2018 -- August 2018] Implementing a hybrid \smt solver \item [August 2018 -- January 2019] Text of Ph.D. thesis. \item [January 2019] The final version of the thesis. \end{description} %***************************************** %***************************************** Loading classicthesis-config.tex +2 −1 Original line number Diff line number Diff line Loading @@ -83,6 +83,7 @@ % Spanish languages need extra options in order to work with this template %\PassOptionsToPackage{spanish,es-lcroman}{babel} \usepackage{babel} \usepackage{enumitem} \usepackage{csquotes} \PassOptionsToPackage{% Loading Loading
Chapters/Chapter03.tex +18 −0 Original line number Diff line number Diff line Loading @@ -6,7 +6,25 @@ \section{Expected Outputs} \newpage \section{Progression Schedule} The plan of my future study and research activities is following: \begin{description}[style=nextline,leftmargin=0.8cm] \item [now -- January 2017] Extension of unconstrained variable propagation to quantified formulas and to non-linear multiplication. \item [January 2017] Doctoral exam and defence of this thesis proposal. \item [January 2017 -- May 2017] Complexity of the quantfied bit-vector formulas without uninterpreted functions and with binary encoded bit-widths. \item [May 2017 -- January 2018] Development of the hybrid approach to \smt solving of quantified bit-vector formulas combining symbolic representation of formulas with \dpllt or \mcsat. \item [January 2018 -- August 2018] Implementing a hybrid \smt solver \item [August 2018 -- January 2019] Text of Ph.D. thesis. \item [January 2019] The final version of the thesis. \end{description} %***************************************** %***************************************** Loading
classicthesis-config.tex +2 −1 Original line number Diff line number Diff line Loading @@ -83,6 +83,7 @@ % Spanish languages need extra options in order to work with this template %\PassOptionsToPackage{spanish,es-lcroman}{babel} \usepackage{babel} \usepackage{enumitem} \usepackage{csquotes} \PassOptionsToPackage{% Loading