Roopsha Samanta
- Assistant Professor
- Department of Computer Science
- Purdue University
- LWSN 2116L CV
I am an Assistant Professor in the Department of Computer Science at Purdue University and a researcher in applied formal methods and automated reasoning. My research seeks to enable programmers formally develop programs that conform to their intent. We develop foundational techniques for algorithmic program verification and synthesis for a spectrum of application domains, correctness specifications, and programmer expertise.
I lead the Purdue Formal Methods (PurForM) group and am a member of the Purdue Programming Languages (PurPL) group. Before joining Purdue in 2016, I completed my PhD at UT Austin in 2013, advised by E. Allen Emerson and Vijay K. Garg, and was a postdoctoral researcher at IST Austria from 2014-2016 with Thomas A. Henzinger. I am a recipient of a 2019 NSF CAREER award and a 2021 Amazon Research Award.
I am not accepting new students, interns, or postdocs in the near future. For more context, please see this post.Select Research
 |
Modular, Bounded Verification of Unbounded Distributed Systems. Modern distributed services are typically built in a modular fashion using core distributed protocols as building blocks. The ubiquity of some of these building blocks has sparked several valiant verification efforts for them in the last decade. Oddly, there have been far fewer verification efforts that go beyond core protocols and target distributed services built on top of such core protocols. In our ambitious Discover[i] project (pronounced, disovery), we seek to develop modular, scalable, fully-automated verification approaches for distributed systems that mimic their modular design. In particular, we advocate an approach based on assuming that the underlying core protocols are verified separately and encapsulating their complexities within cleanly-defined abstractions. See this tutorial or read our OOPSLA 2023 (Venus), TACAS 2023 (Cinnabar), OOPSLA 2021 (QuickSilver) and our CAV 2020 papers to learn more. |
 |
Semantics-Guided Inductive Program Synthesis. Example-based program synthesis and repair are increasingly favored paradigms of program synthesis as they can help democratize programming. Because examples and other inductive specifications are inherently incomplete, inductive synthesis engines encounter challenges such as overfitting, ambiguity, and brittleness, similar to inductive learning-based engines. PL researchers have typically attacked these problems by applying syntactic biases to the search space in the form of tailored DSLs, grammars and ranking functions. We are exploring a variety of techniques to further enhance the generalizability and robustness of such engines by applying semantic biases to the search space. Check out this talk, or read our CAV 2016 Qlose paper and PLDI 2019 SemCluster paper targeting semantics-guided program repair, and our POPL 2020 paper targeting semantics-guided program synthesis. |
 |
Computer-Aided Concurrent Programming. 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. See our FMSD 2017, CAV 2015, and POPL 2015 papers. |
 |
Robustness of I/O Systems.Formalized 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 - and developed automata-theoretic decision procedures for checking K-robustness of discrete transducers, networks of discrete transducers, timed transducers, and asynchronous sequential circuits. See our VMCAI 2016, FSTTCS 2014, ATVA 2013, and VMCAI 2013 papers. |
News
| Sep'22 | Nouraldin Jaber is graduating and joining Amazon S3's Automated Reasoning Group. Congratulations, Nour! |
| Aug'22 | I will be co-editing the ACM SIGPLAN Blog on PL Perspectives with Adrian. We would love to hear from you! |
| Jul'22 | Can't wait for the Dagstuhl workshop I am organizing with Swen Jacobs, Ken McMillan, and Ilya Sergey on Unifying Formal Methods for Trustworthy Distributed Systems. Look out for invitations! |
| Jun'22 | You can now watch our PLDI 2022 tutorial on Discover[i] here! |
| Feb'22 | Nouraldin Jaber, Christopher Wagner, and I will be presenting an invited tutorial on Discover[i] at PLDI 2022 in San Diego! |
| Jan'22 |
New draft from Discover[i] project available: Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems |
All posts |
Select Talks
Research Group
| Nouraldin Jaber (PhD Student, co-supervised with Milind Kulkarni, soon joining Amazon S3-Automated Reasoning Group) |
| Christopher Wagner (PhD Student) |
| Yongwei Yuan (PhD Student) |
| Alumni |
| Xuankang Lin (M.S, 2021, co-supervised with Suresh Jagannathan) |
| David Perry (M.S, 2018, co-supervised with Xiangyu Zhang) |
| Parker Lawrence (Undergraduate Student, Purdue CS) |
| Aarya Barve (Undergraduate Student, Purdue CS) |
| Interns |
| Marcel Moosbrugger (Master's Intern, TU Wien) |
| Yugesh Kuthari (Undergraduate Intern, IIT Kanpur) |
| Mohan Sai Teja Dantam (Undergraduate Intern, IIT Bombay) |
Teaching
| CS592: Neurosymbolic Program Synthesis. Fall 2022 |
| CS560: Reasoning About Programs. Fall 2021, Spring 2021, Spring 2020, Spring 2019, Fall 2017, Fall 2016 |
| CS307: Software Engineering. Spring 2022, Fall 2020, Fall 2019, Spr 2018 |
| CS456: Programming Languages. Spring 2017 |
Professional Activities
| Current Roles | ||
|---|---|---|
| 2022-now | Co-Editor, ACM SIGPLAN Blog on PL Perspectives | |
| 2020-now | Steering Committee, VMWCAV | |
| 2016-now | Steering Committee, DARS | |
| Organization | ||
| 2021 | General Chair MAPSPLDI, Organization Committee VMWCAV | |
| 2020 | Chair VMWCAV | |
| 2019 | Co-Chair PLDI AEC | |
| 2017 | Co-Chair DARSCAV | |
| 2016 | Co-Chair DARSCPSWeek, Publicity Chair CAV | |
| Program Committee | ||
| 2022 | PLDI (Area Chair) | |
| 2021 | PLDI, CAV | |
| 2020 | POPL | |
| 2019 | CAV, PLDI ERC | |
| 2018 | OOPSLA, CAV, VMCAI, SYNT, POPL SRC | |
| 2017 | CAV, FMCAD, SYNT | |
| 2016 | VMCAI, SYNT | |