PolyQEnt: A polynomial quantified entailment solver
Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424.
Download (ext.)
Conference Paper
| Published
| English
Scopus indexed
Author
Chatterjee, KrishnenduISTA 
;
Goharshady, AmirISTA ;
Goharshady, EhsanISTA ;
Karrabi, MehrdadISTA ;
Saadat, Milad;
Seeliger, Maximilian;
Zikelic, DjordjeISTA
;
Goharshady, AmirISTA ;
Goharshady, EhsanISTA ;
Karrabi, MehrdadISTA ;
Saadat, Milad;
Seeliger, Maximilian;
Zikelic, DjordjeISTA Corresponding author has ISTA affiliation
Department
Series Title
LNCS
Abstract
Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints.
Publishing Year
Date Published
2025-10-26
Proceedings Title
23rd International Symposium on Automated Technology for Verification and Analysis
Publisher
Springer Nature
Acknowledgement
This work was supported by the following grants: ERC CoG 863818 (ForM-SMArt), Austrian Science Fund (FWF) 10.55776/COE12, ERC StG 101222524 (SPES), the Ethereum Foundation Research Grant FY24-1793, and the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SISSMU-100).
Volume
16145
Page
411-424
Conference
ATVA: Automated Technology for Verification and Analysis
Conference Location
Bengaluru, India
Conference Date
2025-10-27 – 2025-10-31
ISBN
ISSN
eISSN
IST-REx-ID
Cite this
Chatterjee K, Goharshady AK, Goharshady E, et al. PolyQEnt: A polynomial quantified entailment solver. In: 23rd International Symposium on Automated Technology for Verification and Analysis. Vol 16145. Springer Nature; 2025:411-424. doi:10.1007/978-3-032-08707-2_19
Chatterjee, K., Goharshady, A. K., Goharshady, E., Karrabi, M., Saadat, M., Seeliger, M., & Zikelic, D. (2025). PolyQEnt: A polynomial quantified entailment solver. In 23rd International Symposium on Automated Technology for Verification and Analysis (Vol. 16145, pp. 411–424). Bengaluru, India: Springer Nature. https://doi.org/10.1007/978-3-032-08707-2_19
Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Ehsan Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and Dorde Zikelic. “PolyQEnt: A Polynomial Quantified Entailment Solver.” In 23rd International Symposium on Automated Technology for Verification and Analysis, 16145:411–24. Springer Nature, 2025. https://doi.org/10.1007/978-3-032-08707-2_19.
K. Chatterjee et al., “PolyQEnt: A polynomial quantified entailment solver,” in 23rd International Symposium on Automated Technology for Verification and Analysis, Bengaluru, India, 2025, vol. 16145, pp. 411–424.
Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Saadat M, Seeliger M, Zikelic D. 2025. PolyQEnt: A polynomial quantified entailment solver. 23rd International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 16145, 411–424.
Chatterjee, Krishnendu, et al. “PolyQEnt: A Polynomial Quantified Entailment Solver.” 23rd International Symposium on Automated Technology for Verification and Analysis, vol. 16145, Springer Nature, 2025, pp. 411–24, doi:10.1007/978-3-032-08707-2_19.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)
Access Level
Open Access
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 2408.03796
Google Scholar
ISBN Search