Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
10-2025
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.
Keywords
polynomial quantified entailments, constraint solving, positivity theorems, program analysis
Discipline
Artificial Intelligence and Robotics | Numerical Analysis and Scientific Computing
Areas of Excellence
Digital transformation
Publication
Automated Technology for Verification and Analysis: ATVA 2025: Proceedings, Bengaluru, India, October 27-31
Volume
16145
First Page
411
Last Page
424
ISBN
9783032087072
Identifier
10.1007/978-3-032-08707-2_19
Publisher
Springer
City or Country
Cham
Citation
CHATTERJEE, Krishnendu; GOHARSHADY, Amir Kafshdar; GOHARSHADY, Ehsan Kafshdar; KARRABI, Mehrdad; SAADAT, Milad; SEELIGER, Maximilian; and ZIKELIC, Dorde.
PolyQEnt: A polynomial quantified entailment solver. (2025). Automated Technology for Verification and Analysis: ATVA 2025: Proceedings, Bengaluru, India, October 27-31. 16145, 411-424.
Available at: https://ink.library.smu.edu.sg/sis_research/11166
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-032-08707-2_19
Included in
Artificial Intelligence and Robotics Commons, Numerical Analysis and Scientific Computing Commons