Loading Chapters/Chapter03.tex +27 −1 Original line number Original line Diff line number Diff line Loading @@ -221,7 +221,7 @@ model checker \SymDivine, which uses quantified formulas to decide the equality of two symbolic states. On this set of benchmarks, our solver equality of two symbolic states. On this set of benchmarks, our solver Q3B also has better performance than \smt solvers based on the Q3B also has better performance than \smt solvers based on the quantifier instantiation and bit-blasting. Table xxx shows the numbers quantifier instantiation and bit-blasting. Table xxx shows the numbers of formulas solved by each solver and the Figure yyy presents a cactus of formulas solved by each solver and Figure yyy presents a cactus plot of cpu-times needed to solve these formulas. plot of cpu-times needed to solve these formulas. \begin{table} \begin{table} Loading Loading @@ -284,6 +284,32 @@ can solve as many benchmarks as other solvers, but solves them in the shortest time. Moreover, Q3B can solve more benchmarks with unknown shortest time. Moreover, Q3B can solve more benchmarks with unknown status than any of the other solvers. status than any of the other solvers. \begin{table}[t] \checkoddpage \edef\side{\ifoddpage l\else r\fi} \makebox[\textwidth][\side]{ \begin{minipage}[t]{\fullwidth} \setlength{\tabcolsep}{0.5em} \begin{tabularx}{\textwidth}{l r r r X r r r} \toprule & ~ & \multicolumn{2}{c}{Known status} & & \multicolumn{3}{c}{Unknown status} \\ \cmidrule(l){3-4} \cmidrule(l){6-8} & & \# solved & avg. CPU time & &\# solved & avg. CPU time & avg. WALL time \\ \midrule Boolector & & $85$ & $1.635$ & & $89$ & $11\,431$ & $11\,422$ \\ CVC4 & & $85$ & $1.576$ & & $56$ & $29\,464$ & $29\,453$ \\ Q3B & & $85$ & $0.138$ & & $99$ & $12\,111$ & $4\,059$ \\ Z3 & & $85$ & $0.339$ & & $78$ & $16\,721$ & $16\,713$ \\ \bottomrule \end{tabularx} \caption{Official results of quantified bit-vector category of \smt competition 2016 divided into the benchmarks with known status and benchmarks with a previously unknown status.} \end{minipage}} \end{table} \section{Other areas of research} \section{Other areas of research} Outside the field of \smt solving, my research also consists in Outside the field of \smt solving, my research also consists in software verification. In this field, I have co-authored the following software verification. In this field, I have co-authored the following Loading Loading
Chapters/Chapter03.tex +27 −1 Original line number Original line Diff line number Diff line Loading @@ -221,7 +221,7 @@ model checker \SymDivine, which uses quantified formulas to decide the equality of two symbolic states. On this set of benchmarks, our solver equality of two symbolic states. On this set of benchmarks, our solver Q3B also has better performance than \smt solvers based on the Q3B also has better performance than \smt solvers based on the quantifier instantiation and bit-blasting. Table xxx shows the numbers quantifier instantiation and bit-blasting. Table xxx shows the numbers of formulas solved by each solver and the Figure yyy presents a cactus of formulas solved by each solver and Figure yyy presents a cactus plot of cpu-times needed to solve these formulas. plot of cpu-times needed to solve these formulas. \begin{table} \begin{table} Loading Loading @@ -284,6 +284,32 @@ can solve as many benchmarks as other solvers, but solves them in the shortest time. Moreover, Q3B can solve more benchmarks with unknown shortest time. Moreover, Q3B can solve more benchmarks with unknown status than any of the other solvers. status than any of the other solvers. \begin{table}[t] \checkoddpage \edef\side{\ifoddpage l\else r\fi} \makebox[\textwidth][\side]{ \begin{minipage}[t]{\fullwidth} \setlength{\tabcolsep}{0.5em} \begin{tabularx}{\textwidth}{l r r r X r r r} \toprule & ~ & \multicolumn{2}{c}{Known status} & & \multicolumn{3}{c}{Unknown status} \\ \cmidrule(l){3-4} \cmidrule(l){6-8} & & \# solved & avg. CPU time & &\# solved & avg. CPU time & avg. WALL time \\ \midrule Boolector & & $85$ & $1.635$ & & $89$ & $11\,431$ & $11\,422$ \\ CVC4 & & $85$ & $1.576$ & & $56$ & $29\,464$ & $29\,453$ \\ Q3B & & $85$ & $0.138$ & & $99$ & $12\,111$ & $4\,059$ \\ Z3 & & $85$ & $0.339$ & & $78$ & $16\,721$ & $16\,713$ \\ \bottomrule \end{tabularx} \caption{Official results of quantified bit-vector category of \smt competition 2016 divided into the benchmarks with known status and benchmarks with a previously unknown status.} \end{minipage}} \end{table} \section{Other areas of research} \section{Other areas of research} Outside the field of \smt solving, my research also consists in Outside the field of \smt solving, my research also consists in software verification. In this field, I have co-authored the following software verification. In this field, I have co-authored the following Loading
