Loading [MathJax]/extensions/MathMenu.js
Koushik Sen - IEEE Xplore Author Profile

Showing 1-25 of 44 results

Results

A wide variety of graph algorithms expressed as linear algebra operations, i.e., triangle counting, k-truss analysis, breath first search, betweenness centrality, depend on the masked sparse matrix time sparse matrix multiplication (masked-SpGEMM) kernel. SuiteSparse:GraphBLAS, the de-facto sparse linear algebra library for graph analytics, offers support for this specific computation. Under a sim...Show More
In machine learning programs, it is often tedious to annotate the dimensions of shapes of various tensors that get created during execution. We present a dynamic likely tensor shape inference analysis, called Shapeit, that annotates the dimensions of shapes of tensor expressions with symbolic dimension values and establishes the symbolic relationships among those dimensions. Such annotations can b...Show More
Hybrid program analysis approaches that combine static and dynamic analysis have resulted in powerful tools for automated software testing. In this article, we argue for hybrid techniques that allow minimal but critical intervention from experts to better guide software testing.Show More
Large-scale HPC applications are highly data-intensive with significant times spent in I/O operations. Many large-scale scientific applications do not adequately optimize the I/O operations, leading to overall poor performance. In this work, we have developed two main strategies for providing fast I/O throughput for an important climate modeling application, namely, Regional Ocean Modeling System ...Show More
Visualizations are widely used to communicate findings and make data-driven decisions. Unfortunately creating bespoke and reproducible visualizations requires the use of procedural tools such as matplotlib. These tools present a steep learning curve as their documentation often lacks sufficient usage examples to help beginners get started or accomplish a specific task. Forums such as StackOverflow...Show More
This paper presents Arvada, an algorithm for learning context-free grammars from a set of positive examples and a Boolean-valued oracle. Arvada learns a context-free grammar by building parse trees from the positive examples. Starting from initially flat trees, Arvada builds structure to these trees with a key operation: it bubbles sequences of sibling nodes in the trees into a new node, adding a ...Show More
We present a topology aware quantum synthesis algorithm designed to produce short circuits and to scale well in practice. The main contribution is a novel representation of circuits able to encode placement and topology using generic "gates", which allows the QFAST algorithm to replace expensive searches over circuit structures with few steps of numerical optimization. When compared against optima...Show More
This paper presents a coverage-guided grammar-based fuzzing technique for automatically synthesizing a corpus of concise test inputs. We walk-through a case study of a compiler designed for education and the corresponding problem of generating meaningful test cases to provide to students. The prior state-of-the-art solution is a combination of fuzzing and test-case reduction techniques such as var...Show More
Property-based testing is a popular approach for validating the logic of a program. An effective property-based test quickly generates many diverse valid test inputs and runs them through a parameterized test driver. However, when the test driver requires strict validity constraints on the inputs, completely random input generation fails to generate enough valid inputs. Existing approaches to solv...Show More
We present an algorithm for compiling arbitrary unitaries into a sequence of gates native to a quantum processor. As CNOT gates are error-prone for the foreseeable Noisy-Intermediate-Scale Quantum devices era, our A* inspired algorithm minimizes their count while accounting for connectivity. We discuss the formulation of synthesis as a search problem as well as an algorithm to find solutions. For ...Show More
Previous approaches to dynamic taint analysis for JavaScript are implemented directly in a browser or JavaScript engine, limiting their applicability to a single platform and requiring ongoing maintenance as platforms evolve, or they require nontrivial program transformations. We present an approach that relies on instrumentation to encode taint propagation as instructions for an abstract machine....Show More
The problem of sampling a large number of random solutions to SAT and SMT constraints is essential for constrained-random verification and testing. However, most current sampling techniques lack a problem-specific notion of coverage, considering only general goals such as uniform distribution. We have developed a new technique for coverage-guided sampling that allows the user to specify the desire...Show More
Programs expecting structured inputs often consist of both a syntactic analysis stage, in which raw input is parsed into an internal data structure, and a semantic analysis stage, which conducts checks on this data structure and executes the core logic of the program. Existing random testing tools tend to produce inputs that are rejected early in this pipeline. We propose Zest, a random testing me...Show More
In recent years, fuzz testing has proven itself to be one of the most effective techniques for finding correctness bugs and security vulnerabilities in practice. One particular fuzz testing tool, American Fuzzy Lop (AFL), has become popular thanks to its ease-of-use and bug-finding power. However, AFL remains limited in the bugs it can find since it simply does not cover large regions of code. If ...Show More
Stimulus generation is an essential part of hardware verification, being at the core of widely applied constrained-random verification techniques. However, as verification problems get more and more complex, so do the constraints which must be satisfied. In this context, it is a challenge to efficiently generate random stimuli which can achieve a good coverage of the design space. We developed a n...Show More
Dynamic verification is widely used to increase confidence in the correctness of RTL circuits during the pre-silicon design phase. Despite numerous attempts over the last decades to automate the stimuli generation based on coverage feedback, Coverage Directed Test Generation (CDG) has not found the widespread adoption that one would expect. Based on new ideas from the software testing community ar...Show More
In recent years, several automated GUI testing techniques for Android apps have been proposed. These tools have been shown to be effective in achieving good test coverage and in finding bugs without human intervention. Being automated, these tools typically run for a long time (say, for several hours), either until they saturate test coverage or until a testing time budget expires. Thus, these aut...Show More
In software and hardware testing, generating multiple inputs which satisfy a given set of constraints is an important problem with applications in fuzz testing and stimulus generation. However, it is a challenge to perform the sampling efficiently, while generating a diverse set of inputs which satisfy the constraints. We developed a new algorithm QuickSampler which requires a small number of solv...Show More
Automatic program repair techniques offer the possibility of reducing, or even eliminating, the substantial manual effort that currently goes into the patching of software defects. However, current repair techniques take minutes or hours, to generate rather simple repairs, severely limiting their practical applicability. Search-based program repair represents a popular class of automatic repair te...Show More
Modern web applications are written in an event-driven style, in which event handlers execute asynchronously in response to user or system events. The nondeterminism arising from this programming style can lead to pernicious errors. Recent work focuses on detecting event races and classifying them as harmful or harmless. However, since modifying the source code to prevent harmful races can be a di...Show More
Traversal is one of the most fundamental operations on data structures, in which an algorithm systematically visits some or all of the data items of a data structure. We propose a dynamic analysis technique, called Travioli, for detecting data-structure traversals. We introduce the concept of acyclic execution contexts, which enables precise detection of traversals of arrays and linked data struct...Show More
Many bugs in JavaScript applications manifest themselves as objects that have incorrect property values when a failure occurs. For this type of error, stack traces and log files are often insufficient for diagnosing problems. In such cases, it is helpful for developers to know the control flow path from the creation of an object to a crashing statement. Such crash paths are useful for understandin...Show More
While tremendously useful, automated techniques for tuning the precision of floating-point programs face important scalability challenges. We present Blame Analysis, a novel dynamic approach that speeds up precision tuning. Blame Analysis performs floating-point instructions using different levels of accuracy for their operands. The analysis determines the precision of all operands such that a giv...Show More
We present CATG, an open-source concolic test generation tool for Java and its integration with TesMa, a model-based testing tool which automatically generates test cases from formal design documents. TesMa takes as input a set of design documents of an application under test. The design documents are provided in the form of database table definitions, process-flow diagrams, and screen definitions...Show More
Dynamic languages, such as JavaScript, give programmers the freedom to ignore types, and enable them to write concise code in short time. Despite this freedom, many programs follow implicit type rules, for example, that a function has a particular signature or that a property has a particular type. Violations of such implicit type rules often correlate with problems in the program. This paper pres...Show More