## 8 Experimental Evaluation
### C Standard Libraries  
In the second set of benchmarks (see Table 4), we investigate whether the implementation from several standard libraries matches the expected results of abstract implementation. In other words, we perform an equivalence check of results obtained from M-String operations with the results of the automatically abstracted (originally concrete) standard library functions. We expect that both give the same results. For the evaluation, we picked three open-source libraries: PDClib, musl-libc and \(\mu\)CLibc. Since results for the libraries are rather similar, we present here only an evaluation of PDClib functions. The remaining results are provided in the Supplementary Material. All benchmarks showed that our implementation matches the standard one. Similarly, as in the previous case, these benchmarks suffer from the state space blow up caused by an exponential number of possible character combinations. For this reason, we decreased the size \begin{table}
\begin{tabular}{l r r r r r r r r r r r} \hline \hline  & \multicolumn{4}{c}{**Word**} & \multicolumn{4}{c}{**Sequence**} \\ \cline{2-13}  & \multicolumn{2}{c}{**4**} & \multicolumn{2}{c}{**8**} & \multicolumn{2}{c}{**16**} & \multicolumn{2}{c}{**4**} & \multicolumn{2}{c}{**8**} & \multicolumn{2}{c}{**16**} \\ \cline{2-13}  & \multicolumn{2}{c}{**Time(s)**} & \multicolumn{2}{c}{**States Time(s)**} & \multicolumn{2}{c}{**States Time(s)**} & \multicolumn{2}{c}{**States Time(s)**} & \multicolumn{2}{c}{**States Time(s)**} & \multicolumn{2}{c}{**States Time(s)**} & \multicolumn{2}{c}{**States**} \\ \hline strcmp & 14.3 & 1005 & 105 & 2989 & 1350 & 9741 & 2.17 & 204 & 5.09 & 376 & 16.5 & 720 \\ strcpy & 5.15 & 515 & 57.4 & 1823 & 912 & 6935 & 0.83 & 183 & 2.49 & 347 & 9.14 & 675 \\ strcat & 468 & 5748 & T & – & T & – & 8.56 & 751 & 113 & 2535 & 1940 & 9463 \\ strchr & 0.08 & 22 & 0.08 & 22 & 0.08 & 22 & 0.3 & 17 & 0.3 & 17 & 0.4 & 17 \\ strlen & 0.66 & 91 & 4.13 & 259 & 68.8 & 883 & 0.15 & 34 & 0.28 & 54 & 0.65 & 94 \\ \hline \hline \end{tabular}
\end{table} 
Table 4: Verification results of functions from PDCLib with timeout of 1 h. Measurements show the size of state space and verification time for the parametric length of the input. \begin{table}
\begin{tabular}{l r r r r r r r r r r r r} \hline \hline  & \multicolumn{4}{c}{**Word**} & \multicolumn{4}{c}{**Sequence**} \\ \cline{2-13}  & \multicolumn{4}{c}{**Verification(s)**} & \multicolumn{4}{c}{**Verification(s)**} \\ \cline{2-13}  & \multicolumn{4}{c}{**States**} & \multicolumn{1}{c}{**8**} & \multicolumn{1}{c}{**64**} & \multicolumn{1}{c}{**1024**} & \multicolumn{1}{c}{**4096**} & \multicolumn{1}{c}{**LART(s)**} & \multicolumn{1}{c}{**States**} & \multicolumn{1}{c}{**8**} & \multicolumn{1}{c}{**64**} & \multicolumn{1}{c}{**1024**} & \multicolumn{1}{c}{**4096**} & \multicolumn{1}{c}{**LART(s)**} \\ \hline strcmp & 3562 & 480 & 498 & 472 & 481 & 1.70 & 70 & 0.26 & 0.24 & 0.21 & 0.25 & 1.76 \\ strcpy & 368 & 9.8 & 9.1 & 9.3 & 9.4 & 1.70 & 48 & 0.20 & 0.20 & 0.21 & 0.20 & 1.71 \\ strcat & 7398 & 898 & 873 & 865 & 843 & 1.72 & 105 & 0.51 & 0.52 & 0.53 & 0.51 & 1.72 \\ strchr & 49 & 0.3 & 0.4 & 0.3 & 0.3 & 1.71 & 15 & 0.04 & 0.04 & 0.03 & 0.04 & 1.70 \\ strlen & 78 & 1.1 & 1.2 & 1.0 & 1.3 & 1.70 & 16 & 0.05 & 0.04 & 0.05 & 0.06 & 1.81 \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Measurements of M-String operations on two types of inputs: _Word_ and _Sequence_ described in Section 8.1. Each benchmark measures a size of state space and verification time for input M-Strings of a given length. Lastly, the table shows an average transformation time (LART). All measurements of time are in seconds. The size of state space does not change for different lengths of input—for more details, see discussion in Section 8.1.