PolyQEnt: A Polynomial Quantified Entailment Solver

TL;DR

PolyQEnt is a new tool designed to efficiently solve polynomial quantified entailment problems involving real or integer variables, aiding verification and program analysis tasks.

Contribution

It introduces a unified framework for polynomial quantified entailments and demonstrates its effectiveness over existing SMT solvers through extensive benchmarks.

Findings

PolyQEnt successfully solves a wide range of polynomial quantified entailments.

The tool outperforms existing SMT solvers on benchmark problems.

It provides a practical solution for verification and program analysis involving polynomial constraints.

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.