12 citations · 34 across the 14 of their papers we have counts for
14 papers
ImageEye: Batch Image Processing Using Program Synthesis
Celeste Barnaby, Qiaochu Chen, Roopsha Samanta +1
This paper presents a new synthesis-based approach for batch image processing. Unlike existing tools that can only apply global edits to the entire image, our method can apply fine…
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification (Extended Version)
Nouraldin Jaber, Christopher Wagner, Swen Jacobs +2
Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While…
Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems
Christopher Wagner, Nouraldin Jaber, Roopsha Samanta
The ubiquity of distributed agreement protocols, such as consensus, has galvanized interest in verification of such protocols as well as applications built on top of them. The comp…
HACCLE: Metaprogramming for Secure Multi-Party Computation -- Extended Version
Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik +17
Cryptographic techniques have the potential to enable distrusting parties to collaborate in fundamentally new ways, but their practical implementation poses numerous challenges. An…
Parameterized Verification of Systems with Global Synchronization and Guards
Nouraldin Jaber, Swen Jacobs, Christopher Wagner +2
Inspired by distributed applications that use consensus or other agreement protocols for global coordination, we define a new computational model for parameterized systems that is…
QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement (Extended Version)
Nouraldin Jaber, Christopher Wagner, Swen Jacobs +2
The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far f…
ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Xuankang Lin, He Zhu, Roopsha Samanta +1
Artificial Neural Networks (ANNs) have demonstrated remarkable utility in various challenging machine learning applications. While formally verified properties of their behaviors a…
Program Repair via Direct State Manipulation
Qinheping Hu, Isaac Evavold, Roopsha Samanta +2
The goal of program repair is to automatically fix programs to meet a specification. We propose a new specification mechanism, direct manipulation, in which the programmer can visu…
Optimizing Solution Quality in Synchronization Synthesis
Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger +4
Given a multithreaded program written assuming a friendly, non-preemptive scheduler, the goal of synchronization synthesis is to automatically insert synchronization primitives to…
Lipschitz Robustness of Timed I/O Systems
Thomas A. Henzinger, Jan Otop, Roopsha Samanta
We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of "uncertain inp…
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger +4
We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedu…
Lipschitz Robustness of Finite-state Transducers
Thomas A. Henzinger, Jan Otop, Roopsha Samanta
We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz con…
Cost-Aware Automatic Program Repair
Roopsha Samanta, Oswaldo Olivo, E. Allen Emerson
We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generat…
Towards Algorithmic Synthesis of Synchronization for Shared-Memory Concurrent Programs
Roopsha Samanta
We present a framework that takes a concurrent program composed of unsynchronized processes, along with a temporal specification of their global concurrent behaviour, and automatic…