MaxSMT-решатель, поддерживающий режим портфолио
https://doi.org/10.15514/ISPRAS-2025-37(4)-10
Аннотация
Задача MaxSMT заключается в определении выполнимости формулы теории первого порядка с ограничениями. В статье представлен подход к решению этой задачи для случая бескванторных теорий, которые обычно разрешимы и востребованы на практике для генерации тестов к программному обеспечению. Подход включает в себя модифицированный MaxSAT-алгоритм PrimalDualMaxRes, в котором использование SAT-решателя заменено SMT-решателем, а также реализацию режима портфолио. Последний означает, что итоговый MaxSMT-алгоритм запускается параллельно с несколькими SMT-решателями, и в качестве конечного результата берется наилучший. В качестве SMT-решателей, на базе которых построен режим портфолио, были выбраны Z3, Yices и Bitwuzla. Подход реализован с использованием открытой Kotlin-библиотеки KSMT, реализующей инфраструктуру для работы с набором MaxSMT-решателей. В статье также представлен первый тестовый набор (benchmark) для MaxSMT-задачи. Проведенные эксперименты подтверждают эффективность предложенного решения. Разработанное портфолио MaxSMT-решателей справляется с примерами из тестового набора данных более, чем в четыре раза быстрее существующего MaxSMT-решателя νZ (проект Z3).
Об авторах
Виктория Викторовна ФОМИНА
Санкт-Петербургский государственный университет
Россия
Россия
Аспирант математико-механического факультета СПбГУ. Сфера научных интересов: анализ программ.
Валентин СОБОЛЬ
Университет ИТМО
Россия
Россия
Выпускник Санкт-Петербургского Политехнического университета им. Петра Великого, преподаватель университета ИТМО. Научные интересы: статический анализ программ, символьное исполнение.
Дмитрий Владимирович КОЗНОВ
Санкт-Петербургский государственный университет
Россия
Россия
Доктор технических наук, профессор кафедры системного программирования Санкт-Петербургского государственного университета, Сфера научных интересов: программная инженерия, модельно-ориентированная разработка программного обеспечения, программные данные, машинное обучение.
Список литературы
1. Alouneh, S., Abed, S. E., Al Shayeji, M. H., Mesleh, R. A comprehensive study and analysis on SAT-solvers: advances, usages and achievements. Artificial Intelligence Review, vol. 52, 2019, pp. 2575–2601.
2. Misonizhnik, A., Mordvinov, D. On Satisfiability of Nominal Subtyping with Variance // Proceedings of 33rd European Conference on Object-Oriented Programming (ECOOP 2019), 2019.
3. Barrett, C., Sebastiani, R., Seshia, S. A., Tinelli, C. Satisfiability modulo theories // Handbook of satisfiability. IOS Press, 2021, pp. 1267–1329.
4. Костюков, Ю. О., Батоев, К. А., Мордвинов, Д. А., Костицын, М. П., Мисонижник, А. В. Автоматическое доказательство корректности программ с динамической памятью. Труды ИСП РАН, том 31, вып. 5, 2019 г., стр. 37–62.
5. Barrett, C., Tinelli, C., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y. Satisfiability Modulo Theories: A Beginner’s Tutorial. International Symposium on Formal Methods, 2024, pp. 571– 596.
6. De Moura, L., Bjørner, N. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, March, pp. 337–340.
7. Dutertre, B. Yices 2.2. In International Conference on Computer Aided Verification, 2014, pp. 737–744.
8. Niemetz, A., Preiner, M. Bitwuzla. In International Conference on Computer Aided Verification, 2023, pp. 3–17.
9. Pasareanu, C. S., Phan, Q. S., Malacaria, P. Multi-run side-channel analysis using Symbolic Execution and Max-SMT // Proceedings of IEEE 29th Computer Security Foundations Symposium (CSF). 2016, pp. 387–400.
10. Brockschmidt, M., Larra, D., Oliveras, A., Rodrıguez-Carbonell, E., Rubio, A. Compositional safety verification with Max-SMT // Formal Methods in Computer-Aided Design (FMCAD). 2015, pp. 33–40.
11. Terra-Neves, M., Machado, N., Lynce, I., Manquinho, V. Concurrency debugging with MaxSMT // Proceedings of the AAAI Conference on Artificial Intelligence, vol. 33, No. 01, 2019, pp. 1608–1616.
12. Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A. Proving non-termination using Max-SMT // Proceedings of Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26. Springer, 2014, pp. 779–796.
13. Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A. Proving termination of imperative programs using Max-SMT. In 2013 Formal Methods in Computer-Aided Design, 2013, pp. 218–225.
14. Albert, E., Gordillo, P., Rubio, A., Schett, M. A. Synthesis of super-optimized smart contracts using max-smt. In International conference on computer aided verification, 2020, pp. 177–200.
15. Li, C. M., Manya, F. MaxSAT, hard and soft constraints. In Handbook of satisfiability. IOS Press, 2021, pp. 903–927.
16. Мисонижник А.В., Бабушкин А.А., Морозов С.А., Костюков Ю.О., Мордвинов Д.А., Кознов Д.В. Автоматическое тестирование LLVM-программ со сложными входными структурами данных. Труды ИСП РАН, том 34, вып. 4, 2022 г., стр. 49–62.
17. Chen, T., Zhang, X. S., Guo, S. Z., Li, H. Y., Wu, Y. State of the art: Dynamic symbolic execution for automated test generation. Future Generation Computer Systems, vol. 29(7), 2013, pp. 1758–1773.
18. Bjorner, N., Narodytska, N. Maximum satisfiability using cores and correction sets // Proceedings of Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015, pp. 246–252.
19. Narodytska, N., Bacchus, F. Maximum satisfiability using core-guided MaxSAT resolution // Proceedings of the AAAI Conference on Artificial Intelligence, vol. 28, No. 1, 2014.
20. Morgado, A., Dodaro, C., Marques-Silva, J. Core-Guided MaxSAT with Soft Cardinality Constraints. Principles and Practice of Constraint Programming, 2014, pp. 564–573.
21. Bjørner, N., Phan, A. D., Fleckenstein, L. νz-an optimizing SMT solver // Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21, 2015, pp. 194–199.
22. KSMT, https://github.com/UnitTestBot/ksmt (дата обращения: 01.02.2025).
23. MaxSMT benchmark, https://github.com/viktoriia-fomina/ksmt/releases/tag/0.0.0 (дата обращения: 01.02.2025).
24. SMT-COMP 2023, https://smt-comp.github.io/2023/ (дата обращения: 01.02.2025).
25. GitHub hosted runners, https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners/about-github-hosted-runners (дата обращения: 01.02.2025).
26. Тестовый набор данных для задачи SMT, https://smt-lib.org/benchmarks.shtml (дата обращения: 01.02.2025).
27. Guthmann, O., Strichman, O., Trostanetski, A. Minimal unsatisfiable core extraction for SMT. In 2016 Formal Methods in Computer-Aided Design (FMCAD), 2016, pp. 57–64.
28. Haedicke, F., Frehse, S., Fey, G., Große, D., Drechsler, R. metaSMT: Focus on Your Application not on Solver Integration. 2011, p. 47.
29. Baier, D., Beyer, D., Friedberger, K. JavaSMT 3: Interacting with SMT solvers in Java // Proceedings of International Conference on Computer Aided Verification, 2021, pp. 195-208. DOI: 10.1007/978-3-030-81688-9_9.
30. Gario, M., Micheli, A. PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms // Proceedings of SMT workshop, 2015.
31. Sebastiani, R., Trentin, P. OptiMathSAT: A tool for optimization modulo theories. Journal of Automated Reasoning, 64(3), 2020, pp. 423–460.
32. Cimatti, A., Griggio, A., Schaafsma, B. J., Sebastiani, R. The mathsat5 smt solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2013, pp. 93–107.
33. Sebastiani, R., Trentin, P. On optimization modulo theories, MaxSMT and sorting networks // Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2017, pp. 231–248.
34. Terekhov A.N., Romanovskii K.Y., Koznov D.V., Dolgov P.S., Ivanov A.N. RTST++: Methodology and a CASE tool for the development of information systems and software for real-time systems. Programming and Computer Software, 1999, 25 (5), pp. 276–281.
35. Кознов Д.В., Перегудов А.Ф., Бугайченко Д.Ю., Чернятчик Р.И., Казакова А.С., Павлинов А.А. Визуальная среда проектирования систем телевизионного вещания. Системное программирование, 2006, 2(1), стр. 142–168.
Рецензия
Для цитирования:
ФОМИНА В.В., СОБОЛЬ В., КОЗНОВ Д.В. MaxSMT-решатель, поддерживающий режим портфолио. Труды Института системного программирования РАН. 2025;37(4):177-188. https://doi.org/10.15514/ISPRAS-2025-37(4)-10
For citation:
FOMINA V.V., SOBOL V., KOZNOV D.V. MaxSMT solver with portfolio mode support. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(4):177-188. (In Russ.) https://doi.org/10.15514/ISPRAS-2025-37(4)-10
Послать статью по эл. почте 