TY - GEN
T1 - PSMT
T2 - 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
AU - Jia, Fuqi
AU - Han, Rui
AU - Ma, Xutong
AU - Cui, Baoquan
AU - Liu, Minghao
AU - Huang, Pei
AU - Ma, Feifei
AU - Zhang, Jian
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - SMT (Satisfiability Modulo Theories) has been widely used in program verification, analysis, and test generation. But sometimes, SMT solver outputs incomprehensible solutions, especially for practical instances. Besides, due to the design of the deterministic algorithms, for a given formula, the result of each run is the same. In this paper, we concentrate on combining SMT solving with probability, which will instruct the SMT solver to give some plausible solutions. We define a special problem: PSMT, which allows solving an SMT instance with variables conforming to a certain distribution. We define distribution under constraint for PSMT, which is based on MCSAT (Model Constructing Satisfiability), a mainstream SMT-solving algorithm. We propose the Prob-MCSAT algorithm, which combines the MCSAT algorithm and introduces the probability to variables. The visualized examples show that the resulting assignments will form a clear trend based on Prob-SMT.
AB - SMT (Satisfiability Modulo Theories) has been widely used in program verification, analysis, and test generation. But sometimes, SMT solver outputs incomprehensible solutions, especially for practical instances. Besides, due to the design of the deterministic algorithms, for a given formula, the result of each run is the same. In this paper, we concentrate on combining SMT solving with probability, which will instruct the SMT solver to give some plausible solutions. We define a special problem: PSMT, which allows solving an SMT instance with variables conforming to a certain distribution. We define distribution under constraint for PSMT, which is based on MCSAT (Model Constructing Satisfiability), a mainstream SMT-solving algorithm. We propose the Prob-MCSAT algorithm, which combines the MCSAT algorithm and introduces the probability to variables. The visualized examples show that the resulting assignments will form a clear trend based on Prob-SMT.
KW - Model Constructing Satisfiability
KW - Probability Distribution
KW - Satisfiability Modulo Theories
UR - https://www.scopus.com/pages/publications/85179003935
U2 - 10.1109/ASE56229.2023.00183
DO - 10.1109/ASE56229.2023.00183
M3 - Conference contribution
AN - SCOPUS:85179003935
T3 - Proceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
SP - 1756
EP - 1760
BT - Proceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 11 September 2023 through 15 September 2023
ER -