TY - GEN
T1 - Evaluating SMT Solvers on Schedulability Checking Instances
AU - Metta, Ravindra
AU - Yeolekar, Anand
AU - Chakraborty, Samarjit
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.
PY - 2025
Y1 - 2025
N2 - When using an off-the-shelf Satisfiability Modulo Theory (SMT) solver for solving decision problems, we empirically demonstrate that solver performance is dependent on a number of factors. In particular, these are a combination of (i) constraints modeling the application behaviour, (ii) non-determinism inherent at the application level and the encoding of multiple system behaviours, and (iii) presence (absence) of witnesses, and these can affect solver performance in non-intuitive ways. Further, there is a wide variation in solver performance, e.g., in terms of time and memory consumed across different solvers. Based on controlled experiments on analyzing schedulability problems encoded as SMT formulas, we compare the performance of selected state-of-the-art solvers. Our experiments help develop insights into understanding solver behaviour for domain-specific SMT instances, and help assess the impact of non-determinism on solver performance.
AB - When using an off-the-shelf Satisfiability Modulo Theory (SMT) solver for solving decision problems, we empirically demonstrate that solver performance is dependent on a number of factors. In particular, these are a combination of (i) constraints modeling the application behaviour, (ii) non-determinism inherent at the application level and the encoding of multiple system behaviours, and (iii) presence (absence) of witnesses, and these can affect solver performance in non-intuitive ways. Further, there is a wide variation in solver performance, e.g., in terms of time and memory consumed across different solvers. Based on controlled experiments on analyzing schedulability problems encoded as SMT formulas, we compare the performance of selected state-of-the-art solvers. Our experiments help develop insights into understanding solver behaviour for domain-specific SMT instances, and help assess the impact of non-determinism on solver performance.
KW - Real-Time Systems
KW - SMT solvers
KW - Schedulability analysis
UR - https://www.scopus.com/pages/publications/105000666212
U2 - 10.1007/978-3-031-81981-0_7
DO - 10.1007/978-3-031-81981-0_7
M3 - Conference contribution
AN - SCOPUS:105000666212
SN - 9783031819803
T3 - Communications in Computer and Information Science
SP - 71
EP - 81
BT - Computational Technologies and Electronics - 1st International Conference, ICCTE 2023, Proceedings
A2 - Majumder, Mukta
A2 - Zaman, J. K. M. Sadique Uz
A2 - Ghosh, Mili
A2 - Chakraborty, Samarjit
PB - Springer Science and Business Media Deutschland GmbH
T2 - 1st International Conference on Computational Technologies and Electronics, ICCTE 2023
Y2 - 23 November 2023 through 25 November 2023
ER -