29 citations · 56 across the 14 of their papers we have counts for
14 papers
Existence and Construction of a Gröbner Basis for a Polynomial Ideal
Deepak Kapur, Paliath Narendran
This extended abstract gives a construction for lifting a Gröbner basis algorithm for an ideal in a polynomial ring over a commutative ring R under the condition that R also admits…
Verifying Quantum Phase Estimation (QPE) using Prove-It
Wayne M. Witzel, Warren D. Craft, Robert Carr +1
The general-purpose interactive theorem-proving assistant called Prove-It was used to verify the Quantum Phase Estimation (QPE) algorithm, specifically claims about its outcome pro…
General Interpolation and Strong Amalgamation for Contiguous Arrays
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur +1
Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the dat…
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
Deepak Kapur
Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are pr…
Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version)
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
In this paper, the theory of McCarthy's extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. I…
An Algorithm for Computing a Minimal Comprehensive Gröbner\, Basis of a Parametric Polynomial System
Deepak Kapur, Yiming Yang
An algorithm to generate a minimal comprehensive Gröbner\, basis of a parametric polynomial system from an arbitrary faithful comprehensive Gröbner\, system is presented. A basis o…
Uniform Interpolants in EUF: Algorithms using DAG-representations
Silvio Ghilardi, Alessandro Gianola, Deepak Kapur
The concept of uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the form…
NIL: Learning Nonlinear Interpolants
Mingshuai Chen, Jian Wang, Jie An +3
Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The…
Using Dynamic Analysis to Generate Disjunctive Invariants
ThanhVu Nguyen, Deepak Kapur, Westley Weimer +1
Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invarian…
Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation
ThanhVu Nguyen, Westley Weimer, Deepak Kapur +1
We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthe…
Interpolation synthesis for quadratic polynomial inequalities and combination with EUF
Ting Gan, Liyun Dai, Bican Xia +3
An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict) is proposed. The algorithm is based on…
Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation
Deepak Kapur, Naijun Zhan, Hengjun Zhao
We extend a template-based approach for synthesizing switching controllers for semi-algebraic hybrid systems, in which all expressions are polynomials. This is achieved by combinin…
A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example
Hengjun Zhao, Naijun Zhan, Deepak Kapur +1
In this paper, we propose an approach to reduce the optimal controller synthesis problem of hybrid systems to quantifier elimination; furthermore, we also show how to combine quant…
Unification modulo a partial theory of exponentiation
Deepak Kapur, Andrew Marshall, Paliath Narendran
Modular exponentiation is a common mathematical operation in modern cryptography. This, along with modular multiplication at the base and exponent levels (to different moduli) play…