My research focuses on building reliable and efficient programs using formal methods and programming languages principles.
My work spans the development of mathematical theory, algorithms and tools for program verification, repair and synthesis.
We rely on inspiration and techniques from diverse areas such as automata theory, concurrency theory, logic, model checking, program analyses, machine learning, and control theory.
to learn more.
I am looking for motivated, talented PhD students. If these topics pique your interest, email me!
||Qlose: Program Repair with Quantitative Objectives.
L. D'Antoni, R. Samanta and R. Singh.
CAV 2016. [paper, slides]
||From Non-preemptive to Preemptive Scheduling using
P. Cerny, E. M. Clarke, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach.
CAV 2015. [paper, slides]
||Succinct Representation of Concurrent Trace Sets.
A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta and T. Tarrach.
POPL 2015. [paper, slides]
||Lipschitz Robustness of Finite-state Transducers.
T. A. Henzinger, J. Otop and R. Samanta.
FSTTCS 2014. [paper, slides]
As complex software systems pervade our everyday lives, ensuring their reliability remains a challenge. We must expand our current efforts in at least two directions.
- We must simplify programming.
We should reduce the programmer’s cognitive burden by automating tedious and tricky aspects of programming.
- We must broaden our notion of program reliability beyond correctness.
Most computational systems are embedded in unpredictable environments which may fail to meet their nominal expectations due to corrupt sensors, maliciously injected data, and so on. For such systems, we should additionally aim for robustness: is the change in system behavior, induced by irregularities in the environment, acceptable?
My vision is one of computer-aided programming for development of systems that are correct, efficient and, furthermore, robust. Read on to learn more about ongoing and past projects.
Concurrent data structures present certain design challenges: they must maintain consistency in the presence of concurrent updates without becoming a performance bottleneck. Can we design synthesis techniques for clients of concurrent data structures that target efficiency without sacrificing precision? In this project, we are exploring new application domains and paradigms for performance-aware synthesis.
How do we formalize and analyze robustness of systems (which may or may not be stochastic) in the presence of stochastic disturbances? For instance, how do we check if the behavior of a probabilistic program is "acceptable" when the input distribution is perturbed? The goal of this project is to develop foundational results and practical techniques for the design of robust systems in the presence of stochasticity in the system or its environment.
Quantitative Program Repair for Education
Can we build effective tools for personalized feedback and evaluation of assignments based on inferring "optimal" repairs for student solutions? Can we learn appropriate objective functions, program distances and error models to use for repair from existing databases of assignments? In this project, we are investigating the use of quantitative program repair, along with machine learning, for automated feedback and grading.
Typical concurrency bugs such as data races and deadlocks are often caused by subtle synchronization errors.
In this project, we have developed advanced trace-based techniques for synchronization synthesis and applied them to device driver programming. Our work resulted in new contributions in language theoretic-verification, trace generalization and synchronization inference.
Robustness Analysis of Transducers
In this project, we formalize robustness of finite-state I/O systems as Lipschitz continuity: a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We have studied the K-robustness problem for discrete transducers, networks of discrete transducers, timed transducers, and asynchronous sequential circuits. While checking K-robustness is undecidable even for discrete transducers, we have developed decision procedures for a variety of useful settings.
Roopsha Samanta is an Assistant Professor at Purdue University.
Her research focuses on building reliable and efficient programs using formal methods and programming languages principles.
Her work spans the development of mathematical theory, algorithms and tools for program verification, repair and synthesis. The application domains that her work targets include concurrent systems software, probabilistic and cyber-physical systems, and education technology for programming courses.
Roopsha completed her Ph.D. at The University of Texas at Austin in 2013, supervised by E. Allen Emerson and Vijay K. Garg. From 2014-2016, she was a postdoctoral researcher in Tom Henzinger’s group at the Institute of Science and Technology Austria (IST Austria).