15 citations · 66 across the 23 of their papers we have counts for
4 papers · 1 filter
Quantifier Elimination Meets Treewidth
Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady +3
In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existentia…
PolyQEnt: A Polynomial Quantified Entailment Solver
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady +4
Polynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is…
Polynomial Invariant Generation for Non-deterministic Recursive Programs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady +1
We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial…
Modular Verification for Almost-Sure Termination of Probabilistic Programs
Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee +1
In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable app…