PolyQEnt: A Polynomial Quantified Entailment Solver
Logic in Computer Science
2025-01-30 v3 Programming Languages
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.
Cite
@article{arxiv.2408.03796,
title = {PolyQEnt: A Polynomial Quantified Entailment Solver},
author = {Krishnendu Chatterjee and Amir Kafshdar Goharshady and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and Milad Saadat and Maximilian Seeliger and Đorđe Žikelić},
journal= {arXiv preprint arXiv:2408.03796},
year = {2025}
}