Using reinforcement learning for speeding up the process of SMT solvers with the aim of faster detection of infeasible paths in software

Articles in Press

Document Type : Original Article

Authors

Faculty of Computer Engineering, K. N. Toosi University of Technology

Abstract

Software testing is an important thing in the development process of any software. Most parts of tests are done automatically. In automatic software testing, there may be obstacles that make the test difficult. One of these obstacles is the presence of infeasible paths in the control flow graph. The existence of such paths can cause problems in various fields such as test data generation, security, and etc. and cause resources waste.
To prevent such problems, detecting infeasible paths can be critical. But in large software products, recognizing these paths is time-consuming. In this study, a method has been presented that can increase the detection speed of infeasible paths using reinforcement learning algorithms. In this method, an attempt has been made to increase the speed of SMT solver using DQN. It has been shown that the tactics provided by SMT can be learnt using reinforcement learning, and thus, the speed of solving increases. This way, the speed of all algorithms and methods that use this tool to detect infeasible paths in control flow graphs will also increase.
The method presented in this study has been tested on QF_NRA and QF_NIA logics. In the experiments that have been done, it has been shown that using the proposed method, the speed of the SMT solver can be increased up to 4.7 times.

Keywords

Main Subjects

Soft Computing Journal

Articles in Press, Accepted Manuscript
Available Online from 11 August 2024

Files

History

  • Receive Date: 11 September 2023
  • Revise Date: 27 November 2023
  • Accept Date: 16 January 2024

Share

How to cite

Statistics