82 citations · 84 across the 5 of their papers we have counts for
4 papers
Full-Program Induction: Verifying Array Programs sans Loop Invariants
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
Arrays are commonly used in a variety of software to store and process data in loops. Automatically proving safety properties of such programs that manipulate arrays is challenging…
Matching Multiplications in Bit-Vector Formulas
Supratik Chakraborty, Ashutosh Gupta, Rahul Jain
Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not v…
Balancing Scalability and Uniformity in SAT Witness Generator
Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
Constrained-random simulation is the predominant approach used in the industry for functional verification of complex digital designs. The effectiveness of this approach depends on…
Preservation under Substructures modulo Bounded Cores
Abhisekh Sankaran, Bharat Adsul, Vivek Madan +2
We investigate a model-theoretic property that generalizes the classical notion of "preservation under substructures". We call this property \emph{preservation under substructures…