REVIEW 3 cited by
PolyQEnt: A Polynomial Quantified Entailment Solver
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original 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.
Forward citations
Cited by 3 Pith papers
-
Omega-regular Verification and Control for Distributional Specifications in MDPs
Distributional certificates provide the first automated method for verifying and synthesizing strategies against distributional omega-regular specifications in MDPs.
-
Chance and Mass Interpretations of Probabilities in Markov Decision Processes (Extended Version)
A unified chance and mass framework defines four MDP semantics; reachability is undecidable in one new semantics and #P-hard in the other, with sound algorithms for both.
-
Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
A template-based Skolemization method backed by Positivstellensatz theorems checks many quantified LRA/NRA formulas in subexponential time and returns polynomial witnesses.
Discussion (0). Continue with ORCID to comment.