PolyHorn: A Polynomial Horn Clause Solver
<|reference_start|>PolyHorn: A Polynomial Horn Clause Solver: Polynomial Horn clauses with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyHorn which is a tool for solving polynomial Horn clauses in which variables on both sides of the implication are real valued. Our tool provides a unified framework for polynomial Horn clause solving problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks show the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints.<|reference_end|>
@article{chatterjee2024polyhorn:,
    title={PolyHorn: A Polynomial Horn Clause Solver},
    author={Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar
  Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, {DJ}or{dj}e
  v{Z}ikeli'c},
    journal={arXiv preprint arXiv:2408.03796},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.03796},
    primaryClass={cs.LO cs.PL}
}