Predictive constraint solving and analysis

Alyas Almaawi, Nima Dini, Cagdas Yelen, Milos Gligoric, Sasa Misailovic, Sarfraz Khurshid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 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.

Original languageEnglish (US)
Title of host publicationProceedings - 2020 ACM/IEEE 42nd International Conference on Software Engineering
Subtitle of host publicationNew Ideas and Emerging Results, ICSE-NIER 2020
PublisherIEEE Computer Society
Pages109-112
Number of pages4
ISBN (Electronic)9781450371261
DOIs
StatePublished - Jun 27 2020
Event42nd ACM/IEEE International Conference on Software Engineering: New Ideas and Emerging Results, ICSE-NIER 2020 - Virtual, Online, Korea, Republic of
Duration: Jun 27 2020Jul 19 2020

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Conference

Conference42nd ACM/IEEE International Conference on Software Engineering: New Ideas and Emerging Results, ICSE-NIER 2020
CountryKorea, Republic of
CityVirtual, Online
Period6/27/207/19/20

Keywords

  • Approximate model counting
  • History-aware analysis
  • Korat
  • SAT

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Predictive constraint solving and analysis'. Together they form a unique fingerprint.

Cite this