82 citations · 214 across the 25 of their papers we have counts for
32 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…
On eventual non-negativity and positivity for the weighted sum of powers of matrices
S Akshay, Supratik Chakraborty, Debtanu Pal
The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lie…
Projected Model Counting: Beyond Independent Support
Jiong Yang, Supratik Chakraborty, Kuldeep S. Meel
The past decade has witnessed a surge of interest in practical techniques for projected model counting. Despite significant advancements, however, performance scaling remains the A…
Synthesizing Pareto-Optimal Interpretations for Black-Box Models
Hazem Torfah, Shetal Shah, Supratik Chakraborty +2
We present a new multi-objective optimization approach for synthesizing interpretations that "explain" the behavior of black-box machine learning models. Constructing human-underst…
Diffy: Inductive Reasoning of Array Programs using Difference Invariants
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
We present a novel verification technique to prove interesting properties of a class of array programs with a symbolic parameter N denoting the size of arrays. The technique relies…
A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis
Preey Shah, Aman Bansal, S. Akshay +1
Boolean Skolem function synthesis concerns synthesizing outputs as Boolean functions of inputs such that a relational specification between inputs and outputs is satisfied. This pr…
On synthesizing Skolem functions for first order logic formulae
S. Akshay, Supratik Chakraborty
Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes…
On Uniformly Sampling Traces of a Transition System (Extended Version)
Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi
A key problem in constrained random verification (CRV) concerns generation of input stimuli that result in good coverage of the system's runs in targeted corners of its behavior sp…
Verifying Array Manipulating Programs with Full-Program Induction
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
We present a full-program induction technique for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N. In…
Knowledge Compilation for Boolean Functional Synthesis
S. Akshay, Jatin Arora, Supratik Chakraborty +3
Given a Boolean formula F(X,Y), where X is a vector of outputs and Y is a vector of inputs, the Boolean functional synthesis problem requires us to compute a Skolem function vector…
On Symbolic Approaches for Computing the Matrix Permanent
Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi
Counting the number of perfect matchings in bipartite graphs, or equivalently computing the permanent of 0-1 matrices, is an important combinatorial problem that has been extensive…
A Generalization of the Łoś-Tarski Preservation Theorem - Dissertation Summary
Abhisekh Sankaran
This article gives a summary of the author's Ph.D. dissertation (arXiv:1609.06297). In addition to an overview of notions and results, it also provides sketches of various proofs a…
Functional Synthesis via Input-Output Separation
Supratik Chakraborty, Dror Fried, Lucas M. Tabajara +1
Boolean functional synthesis is the process of constructing a Boolean function from a Boolean specification that relates input and output variables. Despite significant recent deve…
What's hard about Boolean Functional Synthesis
S. Akshay, Supratik Chakraborty, Shubham Goel +2
Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the…
Demand-driven Alias Analysis : Formalizing Bidirectional Analyses for Soundness and Precision
Swati Jaiswal, Uday P. Khedker, Supratik Chakraborty
A demand-driven approach to program analysis have been viewed as efficient algorithms to compute only the information required to serve a target demand. In contrast, an exhaustive…
On Petri Nets with Hierarchical Special Arcs
S. Akshay, Supratik Chakraborty, Ankush Das +2
We investigate the decidability of termination, reachability, coverability and deadlock-freeness of Petri nets endowed with a hierarchy on places, and with inhibitor arcs, reset ar…
Verifying Array Manipulating Programs by Tiling
Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a…
Towards Parallel Boolean Functional Synthesis
S. Akshay, Supratik Chakraborty, Ajith K. John +1
Given a relational specification R(X, Y), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the spe…
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…
Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
Kuldeep S. Meel, Moshe Vardi, Supratik Chakraborty +5
Constrained sampling and counting are two fundamental problems in artificial intelligence with a diverse range of applications, spanning probabilistic reasoning and planning to con…
Approximate Probabilistic Inference via Word-Level Counting
Supratik Chakraborty, Kuldeep S. Meel, Rakesh Mistry +1
Hashing-based model counting has emerged as a promising approach for large-scale probabilistic inference on graphical models. A key component of these techniques is the use of xor-…
Skolem Functions for Factored Formulas
Ajith K. John, Shetal Shah, Supratik Chakraborty +2
Given a propositional formula F(x,y), a Skolem function for x is a function Ψ(y), such that substituting Ψ(y) for x in F gives a formula semantically equivalent to \exists F. Autom…
Word-level Symbolic Trajectory Evaluation
Supratik Chakraborty, Zurab Khasidashvili, Carl-Johan H. Seger +4
Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify industrial designs. Existing implementations of STE, however, reason at…
Distribution-Aware Sampling and Weighted Model Counting for SAT
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel +2
Given a CNF formula and a weight for each assignment of values to variables, two natural problems are weighted model counting and distribution-aware sampling of satisfying assignme…