## Table: Function Verification Performance Across Tools ### Overview This table compares the verification performance (verification count "vc" and time "atime") of various formal verification tools (Alt-Ergo, CVC3, CVC4, Eprover, Spass, Z3) across 30+ functions. Checkmarks (✓) indicate successful verification, while numerical values represent time in seconds. Color-coded cells highlight performance outliers (red: high time, green: low time, blue: moderate). ### Components/Axes - **Rows**: Functions (e.g., `_parse_integ`, `check_bytes8`, `memmove`, `strncmp`). - **Columns**: Tools with versions: - Alt-Ergo 1.30 - CVC3 2.4.1 - CVC4 1.4 - CVC4 1.5 - Eprover 1.9.1-001 - Spass 3.9 - Z3 4.5.0 - **Legend**: - ✓ = Verified (vc) - Numerical values = Time (atime, seconds) - Colors: - Red: High time (>5s) - Green: Low time (<1s) - Blue: Moderate time (1-5s) ### Detailed Analysis | Function | vc_total | Alt-Ergo 1.30 (vc/atime) | CVC3 2.4.1 (vc/atime) | CVC4 1.4 (vc/atime) | CVC4 1.5 (vc/atime) | Eprover 1.9.1-001 (vc/atime) | Spass 3.9 (vc/atime) | Z3 4.5.0 (vc/atime) | |-------------------|----------|--------------------------|------------------------|----------------------|----------------------|-------------------------------|-----------------------|----------------------| | `_parse_integ` | 282 | 276 (0.10) | 280 (0.83) | ✓ (0.18) | ✓ (0.10) | 212 (0.24) | 197 (1.69) | 279 (0.06) | | `check_bytes8` | 50 | 49 (0.55) | 49 (0.09) | ✓ (0.09) | ✓ (0.11) | 38 (1.76) | 31 (8.38) | 36 (1.52) | | `kstrtobool` | 1096 | ✓ (0.05) | ✓ (0.08) | ✓ (0.10) | ✓ (0.09) | 1006 (0.13) | 937 (0.38) | 1065 (0.15) | | `memchr` | 39 | ✓ (6.05) | 11 (0.22) | ✓ (0.37) | ✓ (0.15) | 31 (2.58) | 11 (5.73) | 29 (0.12) | | `memcmp` | 60 | 58 (0.13) | ✓ (0.15) | ✓ (0.10) | ✓ (0.10) | 49 (0.51) | 36 (4.45) | 55 (0.15) | | `memcpy` | 43 | ✓ (4.18) | ✓ (0.35) | ✓ (0.16) | ✓ (0.14) | 30 (1.05) | 16 (6.85) | 30 (0.06) | | `memmove` | 93*92 | 90 (3.94) | ✓ (0.88) | ✓ (0.16) | ✓ (0.18) | 63 (0.95) | 43 (11.87) | 68 (0.30) | | `memscan` | 47 | 46 (0.07) | ✓ (0.10) | ✓ (0.09) | ✓ (0.09) | 41 (0.59) | 34 (4.55) | 42 (0.06) | | `memset` | 27 | 26 (5.02) | 14 (0.19) | ✓ (0.19) | ✓ (0.16) | 19 (3.82) | 12 (11.12) | 18 (0.08) | | `skip_spaces` | 34 | 30 (0.76) | 1.96 (1.96) | ✓ (0.14) | ✓ (0.34) | 27 (0.70) | 24 (0.34) | 30 (0.09) | | `strcasecmp` | 58 | 50 (0.43) | 1.65 (1.65) | ✓ (0.53) | ✓ (0.53) | 43 (0.28) | 35 (2.85) | 49 (0.49) | | `strcat` | 73 | 68 (0.58) | 2.16 (2.16) | ✓ (0.17) | ✓ (0.17) | 54 (2.56) | 39 (0.67) | 60 (0.94) | | `strchr` | 43 | 35 (4.57) | 23 (0.17) | ✓ (0.23) | ✓ (0.22) | 31 (1.03) | 24 (3.65) | 32 (0.11) | | `strchr_nul` | 46 | 42 (2.07) | 0.26 (0.26) | ✓ (0.19) | ✓ (0.16) | 40 (1.91) | 31 (2.27) | 39 (0.31) | | `strcmp` | 60 | 51 (1.76) | 16 (0.60) | ✓ (0.60) | ✓ (1.08) | 47 (1.05) | 36 (1.65) | 47 (0.10) | | `strcpy` | 46 | 43 (1.33) | 0.66 (0.66) | ✓ (0.17) | ✓ (0.17) | 33 (1.13) | 26 (0.65) | 39 (1.43) | | `strcspn` | 78 | 68 (0.38) | 0.37 (0.37) | ✓ (2.95) | ✓ (1.82) | 58 (1.85) | 46 (1.68) | 61 (0.11) | | `strlcpy` | 84 | 82 (0.15) | 0.14 (0.14) | ✓ (1.08) | ✓ (0.24) | 67 (1.20) | 52 (1.74) | 78 (0.42) | | `strlen` | 26 | ✓ (1.12) | 0.12 (0.12) | ✓ (0.16) | ✓ (0.23) | 19 (3.36) | 14 (2.96) | 21 (0.08) | | `strnchr` | 49 | 38 (4.44) | 19 (0.23) | ✓ (0.23) | ✓ (0.23) | 35 (2.57) | 24 (1.56) | 27 (0.09) | | `strncmp` | 102 | 81 (2.57) | 25 (0.25) | ✓ (0.25) | ✓ (2.32) | 76 (1.06) | 55 (2.56) | 76 (0.57) | | `strnlen` | 44 | 39 (1.91) | 1.04 (1.04) | ✓ (1.23) | ✓ (1.31) | 31 (2.40) | 26 (5.52) | 32 (0.08) | | `strpbrk` | 70 | 57 (0.64) | 1.54 (1.54) | ✓ (3.18) | ✓ (1.57) | 48 (1.89) | 39 (0.75) | 53 (0.09) | | `strrchr` | 62 | 53 (4.57) | 12 (0.17) | ✓ (1.09) | ✓ (0.85) | 46 (2.33) | 31 (4.67) | 46 (0.11) | | `strsep` | 62 | 60 (0.25) | 0.09 (0.09) | ✓ (0.19) | ✓ (0.15) | 55 (0.12) | 51 (1.48) | 58 (0.06) | | `strspn` | 107 | 99 (0.84) | 0.69 (0.69) | ✓ (1.32) | ✓ (0.61) | 89 (1.37) | 75 (1.59) | 91 (0.13) | | **TOTAL** | 2781 | 2645 (0.90) | 2454 (0.42) | 2740 (0.61) | 2761 (0.37) | 2288 (0.76) | 1945 (1.72) | 2461 (0.22) | ### Key Observations 1. **Z3 4.5.0** dominates in total verification count (2461 vc) and has the lowest average time (0.22s), suggesting superior efficiency. 2. **CVC4 1.5** shows mixed performance: high vc (2761) but moderate times (0.37s avg), indicating reliability with slight latency. 3. **Spass 3.9** has the highest total time (1.72s avg) and lower vc (1945), suggesting slower but still effective verification. 4. **Eprover 1.9.1-001** has the lowest vc (2288) but moderate times (0.76s avg), indicating potential limitations in handling complex functions. 5. **Alt-Ergo 1.30** performs well for simple functions (e.g., `check_bytes8` at 0.05s) but struggles with complex ones (e.g., `memmove` at 3.94s). 6. **CVC3 2.4.1** has the lowest vc (2454) and moderate times (0.42s avg), suggesting outdated or less optimized capabilities. ### Interpretation The data reveals significant disparities in tool performance: - **Z3 4.5.0** is the most efficient, verifying nearly all functions quickly (e.g., `memmove` in 0.30s). - **CVC4 1.5** balances reliability and speed, though its time spikes (e.g., `strcspn` at 2.95s) suggest occasional bottlenecks. - **Spass 3.9** and **Eprover** lag in speed but still verify most functions, indicating niche use cases. - **Alt-Ergo 1.30** excels in low-time verification for simple tasks but falters with complex ones, highlighting version limitations. - **CVC3 2.4.1** underperforms across metrics, likely due to outdated algorithms or lack of optimization. This analysis underscores the importance of tool selection based on function complexity and performance requirements. Z3 4.5.0 emerges as the optimal choice for most scenarios, while CVC4 1.5 offers a reliable alternative for time-sensitive tasks.