Roopsha Samanta

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. Click here to learn more.

I am looking for motivated, talented PhD students. If these topics pique your interest, email me!

News
June'17 Invited talk in PLMW@PLDI 2017
Jan'17 Panelist in PLMW@POPL 2017
Dec'16 Co-chairing DARS 2017 (colocated with CAV 2017)
Dec'16 Serving on the PC of SYNT 2017
Dec'16 Serving on the PC of FMCAD 2017
Sep'16 New journal paper in FMSD
More
Selected publications
1. Qlose: Program Repair with Quantitative Objectives.
L. D'Antoni, R. Samanta and R. Singh.
CAV 2016. [paper, slides]
2. From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis.
P. Cerny, E. M. Clarke, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach.
CAV 2015. [paper, slides]
3. Succinct Representation of Concurrent Trace Sets.
A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta and T. Tarrach.
POPL 2015. [paper, slides]
4. Lipschitz Robustness of Finite-state Transducers.
T. A. Henzinger, J. Otop and R. Samanta.
FSTTCS 2014. [paper, slides]
Research
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.

Performance-aware Synthesis
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.

Stochastic Robustness
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.
Publications [SAS14], [CAV16]
Tools Qlose

Synchronization Synthesis
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.
Publications [POPL15], [CAV15], [FMSD16]
Tools TARA, LISS, LIMI

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.
Publications [VMCAI13], [ATVA13], [FSTTCS14], [VMCAI16]
Conference papers
  1. Qlose: Program Repair with Quantitative Objectives.
    L. D'Antoni, R. Samanta and R. Singh.
    CAV 2016. [paper, slides]
  2. Lipschitz Robustness of Timed I/O Systems.
    T. A. Henzinger, J. Otop and R. Samanta.
    VMCAI 2016. [paper]
  3. From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis.
    P. Cerny, E. M. Clarke, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach.
    CAV 2015. [paper, slides]
  4. Succinct Representation of Concurrent Trace Sets.
    A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta and T. Tarrach.
    POPL 2015. [paper, slides]
  5. Lipschitz Robustness of Finite-state Transducers.
    T. A. Henzinger, J. Otop and R. Samanta.
    FSTTCS 2014. [paper, slides]
  6. Cost-aware Program Repair.
    R. Samanta, O. Olivo and E. A. Emerson.
    SAS 2014. [paper, slides]
  7. Robustness Analysis of String Transducers.
    R. Samanta, J. V. Deshmukh and S. Chaudhuri.
    ATVA 2013. [paper, slides]
  8. Robustness Analysis of Networked Systems.
    R. Samanta, J. V. Deshmukh and S. Chaudhuri.
    VMCAI 2013. [paper, slides]
  9. An Algorithmic Framework for Synthesis of Concurrent Programs.
    E. A. Emerson and R. Samanta.
    ATVA 2011. [paper, slides]
  10. Automatic Generation of Local Repairs for Boolean Programs.
    R. Samanta, J. V. Deshmukh and E. A. Emerson.
    FMCAD 2008. [paper, slides]
  11. Codebook Adaptation for Quantized MIMO Beamforming Systems.
    R. Samanta and R. W. Heath, Jr.
    IEEE Asilomar Conference on Signals, Systems, and Computers 2005. [paper]
  12. Frame Theoretic Quantization of Limited Feedback MIMO Beamforming Systems.
    B. Mondal, R. Samanta, and R. W. Heath, Jr.
    Wireless Networks, Communications and Mobile Computing 2005. [paper]
  13. Joint Space-Time Interference Cancellation and Channel Shortening.
    R. Samanta, R. W. Heath, Jr., and B. L. Evans.
    IEEE Asilomar Conference on Signals, Systems, and Computers 2003. [paper]
Journal Papers
  1. From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis.
    P. Cerny, E. M. Clarke, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach.
    Formal Methods in System Design 2016. [paper]
  2. On the Voronoi Tessellations of a Sphere by an Equiangular Unit Norm Frame.
    B. Mondal, R. Samanta, and R. W. Heath, Jr.
    Applied and Computational Harmonic Analysis 2007. [paper]
  3. Joint Interference Cancellation and Channel Shortening for Multi-User MIMO Systems.
    R. Samanta, R. W. Heath, Jr., and B. L. Evans.
    IEEE Transactions on Vehicular Technology 2007. [paper]
Workshop Papers
  1. Towards Algorithmic Synthesis of Synchronization for Shared-Memory Concurrent Programs.
    R. Samanta.
    SYNT 2012. [paper, slides]
Technical Reports
  1. Optimizing Solution Quality in Synchronization Synthesis.
    P. Cerny, E. M. Clarke, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach.
    ArXiv e-prints 2015, arXiv:1511.07163. [paper]
  2. Economical Tranformations for Structured Data.
    J. V. Deshmukh, E. A. Emerson and R. Samanta.
    The University of Texas at Austin, Department of Computer Sciences, Technical Report TR-10-28 2010. [paper]
Theses
  1. Program Reliability through Algorithmic Design and Analysis.
    Ph.D. Dissertation. The University of Texas at Austin 2013. [dissertation]
  2. Joint Space-Time Interference Cancellation and Channel Shortening.
    Master's Report. The University of Texas at Austin 2003. [report]
Patents
  1. Link Performance Prediction Presence of Co-channel Interference.
    N. Himayat, R. Samanta, and S. Talwar.
    US Patent 7,697,906. Awarded 2010.
  2. MIMO Precoding in the Presence of Co-channel Interference.
    S. Talwar, R. Samanta, and N. Himayat.
    US Patent Application 20,070/211,813. Filed 2006.


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).

CV