52 citations · 120 across the 14 of their papers we have counts for
16 papers
Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs
Ashish Mishra, Suresh Jagannathan
Parser combinators are a well-known mechanism used for the compositional construction of parsers, and have shown to be particularly useful in writing parsers for rich grammars with…
Polymorphic Coverage Types
Zhe Zhou, Ashish Mishra, Benjamin Delaware +1
Test input generators are an important part of property-based testing (PBT) frameworks, and a key expectation is that they be capable of producing all acceptable elements that sati…
Specification-Guided Component-Based Synthesis from Effectful Libraries
Ashish Mishra, Suresh Jagannathan
Component-based synthesis seeks to build programs using the APIs provided by a set of libraries. Oftentimes, these APIs have effects, which make it challenging to reason about the…
Data-Driven Abductive Inference of Library Specifications
Zhe Zhou, Robert Dickerson, Benjamin Delaware +1
Programmers often leverage data structure libraries that provide useful and reusable abstractions. Modular verification of programs that make use of these libraries naturally rely…
Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning
Zikang Xiong, Suresh Jagannathan
There has been significant recent interest in devising verification techniques for learning-enabled controllers (LECs) that manage safety-critical systems. Given the opacity and la…
Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring
Kia Rahmani, Kartik Nagar, Benjamin Delaware +1
Serializability is a well-understood concurrency control mechanism that eases reasoning about highly-concurrent database programs. Unfortunately, enforcing serializability has a hi…
Robustness to Adversarial Attacks in Learning-Enabled Controllers
Zikang Xiong, Joe Eappen, He Zhu +1
Learning-enabled controllers used in cyber-physical systems (CPS) are known to be susceptible to adversarial attacks. Such attacks manifest as perturbations to the states generated…
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
Kartik Nagar, Prasita Mukherjee, Suresh Jagannathan
Geo-replicated systems provide a number of desirable properties such as globally low latency, high availability, scalability, and built-in fault tolerance. Unfortunately, programmi…
CLOTHO: Directed Test Generation for Weakly Consistent Database Systems
Kia Rahmani, Kartik Nagar, Benjamin Delaware +1
Relational database applications are notoriously difficult to test and debug. Concurrent execution of database transactions may violate complex structural invariants that constrain…
An Inductive Synthesis Framework for Verifiable Reinforcement Learning
He Zhu, Zikang Xiong, Stephen Magill +1
Despite the tremendous advances that have been made in the last decade on developing useful machine-learning applications, their wider adoption has been hindered by the lack of str…
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…
Automated Parameterized Verification of CRDTs
Kartik Nagar, Suresh Jagannathan
Maintaining multiple replicas of data is crucial to achieving scalability, availability and low latency in distributed applications. Conflict-free Replicated Data Types (CRDTs) are…
Automated Detection of Serializability Violations under Weak Consistency
Kartik Nagar, Suresh Jagannathan
While a number of weak consistency mechanisms have been developed in recent years to improve performance and ensure availability in distributed, replicated systems, ensuring correc…
Alone Together: Compositional Reasoning and Inference for Weak Isolation
Gowtham Kaki, Kartik Nagar, Mahsa Nazafzadeh +1
Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other whi…
Building Resource Adaptive Software Systems (BRASS): Objectives and System Evaluation
Jeffrey Hughes, Cassandra Sparks, Alley Stoughton +3
As modern software systems continue inexorably to increase in complexity and capability, users have become accustomed to periodic cycles of updating and upgrading to avoid obsolesc…
High Quality of Service on Video Streaming in P2P Networks using FST-MDC
Suresh Jaganathan, Jeevan Eranti
Video streaming applications have newly attracted a large number of participants in a distribution network. Traditional client-server based video streaming solutions sustain precio…