The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Boosting SMT solver performance on mixed-bitwise-arithmetic expressions
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
Satisfiability Modulo Theories (SMT) solvers have been widely applied in automated software analysis to reason about the queries that encode the essence of program semantics, relieving the heavy burden of manual analysis. Many SMT solving techniques rely on solving Boolean satisfiability problem (SAT), which is an NP-complete problem, so they use heuristic search strategies to seek possible solutions, especially when no known theorem can efficiently reduce the problem. An emerging challenge, named Mixed-Bitwise-Arithmetic (MBA) obfuscation, impedes SMT solving by constructing identity equations with both bitwise operations (and, or, negate) and arithmetic computation (add, minus, multiply). Common math theorems for bitwise or arithmetic computation are inapplicable to simplifying MBA equations, leading to performance bottlenecks in SMT solving.
@misc{xu2021boosting,
title = {Boosting SMT solver performance on mixed-bitwise-arithmetic expressions},
author = {Dongpeng Xu and Binbin Liu and Weijie Feng and Jiang Ming and Qilong Zheng and Jing Li and Qiaoyan Yu},
year = {2021},
journal = {ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
pages = {651--664},
doi = {10.1145/3453483.3454068},
}