82 citations · 214 across the 25 of their papers we have counts for
19 papers · 1 filter
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…
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…
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…
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…
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…
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…
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…
A Generalization of the Łoś-Tarski Preservation Theorem over Classes of Finite Structures
Abhisekh Sankaran, Bharat Adsul, Supratik Chakraborty
We investigate a generalization of the Łoś-Tarski preservation theorem via the semantic notion of \emph{preservation under substructures modulo -sized cores}. It was shown earli…
A Scalable Approximate Model Counter
Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
Propositional model counting} (#SAT), i.e., counting the number of satisfying assignments of a propositional formula, is a problem of significant theoretical and practical interest…
A Scalable and Nearly Uniform Generator of SAT Witnesses
Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
Functional verification constitutes one of the most challenging tasks in the development of modern hardware systems, and simulation-based verification techniques dominate the funct…
Generalizations of the Los-Tarski Preservation Theorem
Abhisekh Sankaran, Bharat Adsul, Supratik Chakraborty
We present new preservation theorems that semantically characterize the and prefix classes of first order logic, for each natural number…
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…
On Semantic Generalizations of the Bernays-Schönfinkel-Ramsey Class with Finite or Co-finite Spectra
Abhisekh Sankaran, Supratik Chakraborty
Motivated by model-theoretic properties of the BSR class, we present a family of semantic classes of FO formulae with finite or co-finite spectra over a relational vocabulary Σ. A…