PolyQEnt: A Polynomial Quantified Entailment Solver
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915127503093760 |
|---|---|
| author | Chatterjee, Krishnendu Goharshady, Amir Kafshdar Goharshady, Ehsan Kafshdar Karrabi, Mehrdad Saadat, Milad Seeliger, Maximilian Žikelić, Đorđe |
| author_facet | Chatterjee, Krishnendu Goharshady, Amir Kafshdar Goharshady, Ehsan Kafshdar Karrabi, Mehrdad Saadat, Milad Seeliger, Maximilian Žikelić, Đorđe |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_03796 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | PolyQEnt: A Polynomial Quantified Entailment Solver Chatterjee, Krishnendu Goharshady, Amir Kafshdar Goharshady, Ehsan Kafshdar Karrabi, Mehrdad Saadat, Milad Seeliger, Maximilian Žikelić, Đorđe Logic in Computer Science Programming Languages 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. |
| title | PolyQEnt: A Polynomial Quantified Entailment Solver |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2408.03796 |