TY - GEN
T1 - Predictive constraint solving and analysis
AU - Almaawi, Alyas
AU - Dini, Nima
AU - Yelen, Cagdas
AU - Gligoric, Milos
AU - Misailovic, Sasa
AU - Khurshid, Sarfraz
N1 - Publisher Copyright:
© 2020 ACM.
PY - 2020/6/27
Y1 - 2020/6/27
N2 - We introduce a new idea for enhancing constraint solving engines that drive many analysis and synthesis techniques that are powerful but have high complexity. Our insight is that in many cases the engines are run repeatedly against input constraints that encode problems that are related but of increasing complexity, and domainspecific knowledge can reduce the complexity. Moreover, even for one formula the engine may perform multiple expensive tasks with commonalities that can be estimated and exploited. We believe these relationships lay a foundation for making the engines more effective and scalable. We illustrate the viability of our idea in the context of a well-known solver for imperative constraints, and discuss how the idea generalizes to more general purpose methods.
AB - We introduce a new idea for enhancing constraint solving engines that drive many analysis and synthesis techniques that are powerful but have high complexity. Our insight is that in many cases the engines are run repeatedly against input constraints that encode problems that are related but of increasing complexity, and domainspecific knowledge can reduce the complexity. Moreover, even for one formula the engine may perform multiple expensive tasks with commonalities that can be estimated and exploited. We believe these relationships lay a foundation for making the engines more effective and scalable. We illustrate the viability of our idea in the context of a well-known solver for imperative constraints, and discuss how the idea generalizes to more general purpose methods.
KW - Approximate model counting
KW - History-aware analysis
KW - Korat
KW - SAT
KW - History-Aware analysis
KW - approximate model counting
UR - http://www.scopus.com/inward/record.url?scp=85093666573&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85093666573&partnerID=8YFLogxK
U2 - 10.1145/3377816.3381740
DO - 10.1145/3377816.3381740
M3 - Conference contribution
AN - SCOPUS:85104645677
T3 - Proceedings - International Conference on Software Engineering
SP - 109
EP - 112
BT - Proceedings - 2020 ACM/IEEE 42nd International Conference on Software Engineering
PB - IEEE Computer Society
T2 - 42nd ACM/IEEE International Conference on Software Engineering: New Ideas and Emerging Results, ICSE-NIER 2020
Y2 - 27 June 2020 through 19 July 2020
ER -