@inproceedings{7f26f7b204ae423cbff7d6d062617b3f,
title = "Predictive Constraint Solving and Analysis",
abstract = "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 domain-specific 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. ",
keywords = "History-Aware analysis, Korat, SAT, approximate model counting",
author = "Alyas Almaawi and Nima Dini and Cagdas Yelen and Milos Gligoric and Sasa Misailovic and Sarfraz Khurshid",
note = "Funding Information: We thank the anonymous reviewers and Marko Vasic for valuable comments. This work was partially supported by NSF grants CCF-1703637, CCF-1704790, and CCF-1846354, and a Facebook Testing and Verification Research Award. Publisher Copyright: {\textcopyright} 2020 ACM.; 42nd ACM/IEEE International Conference on Software Engineering: New Ideas and Emerging Results, ICSE-NIER 2020 ; Conference date: 27-06-2020 Through 19-07-2020",
year = "2020",
month = oct,
doi = "10.1145/3377816.3381740",
language = "English (US)",
series = "Proceedings - 2020 ACM/IEEE 42nd International Conference on Software Engineering: New Ideas and Emerging Results, ICSE-NIER 2020",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "109--112",
booktitle = "Proceedings - 2020 ACM/IEEE 42nd International Conference on Software Engineering",
address = "United States",
}