I am a Computing and Mathematical Sciences postdoctoral scholar at the California Institute of Technology,
where I work with Richard Murray and Sanjit Seshia.
My research explores algorithmic methods for designing and controlling autonomous systems, guaranteeing correctness with respect to formal specifications. I focus on safety-critical systems performing complex tasks in adversarial environments, interacting with a variety of agents. I draw on technical and creative perspectives from formal methods for software verification, hybrid systems, robotics, control and game theory.
I earned a Ph.D. in 2013 from the Department of Computer Science at Cornell University, where I was advised by Hadas Kress-Gazit and affiliated with the Autonomous Systems Lab and the LTLMoP Project. My dissertation addressed challenges in the synthesis of provably correct control for robotics. I also hold a B.A. in Computer Science and Mathematics from Wellesley College.
Key Research Projects
- Provably Correct Control for Collaborative Robot Teams
- Model Predictive Control Synthesis from Timed Logics
- Timing Semantics for Controller Synthesis from High-Level Specifications
- Explaining Unsynthesizable Specifications For High-Level Robot Behavior
- Epistemic Characterization of Cryptographic Concepts Using Modal Logic
- C. Lignos, V. Raman, C. Finucane, M. Marcus, H. Kress-Gazit, Provably Correct Reactive Control from Natural Language, Autonomous Robots, 38(1): 89-105, 2015. [pdf]
- V. Raman, H. Kress-Gazit, Unsynthesizable Cores -- Minimal Explanations for Unsynthesizable High-Level Robot Behaviors, In submission.
- V. Raman, N. Piterman, C. Finucane, H. Kress-Gazit, Timing Semantics for Abstraction and Execution of Synthesized High-Level Robot Control, IEEE Transactions on Robotics, To appear, 2015. [pdf]
- V. Raman, H. Kress-Gazit, Explaining Impossible High-Level Robot Behaviors, IEEE Transactions on Robotics, 29(1): 94-104, 2013. [pdf]
- J. DeCastro, V. Raman, H. Kress-Gazit, Dynamics-Driven Adaptive Abstraction for Reactive High-Level Mission and Motion Planning, ICRA 2015 (To appear). [pdf] [slides]
- M. Fält, V. Raman, R. M. Murray, Variable Elimination for Scalable Receding Horizon Temporal Logic, ACC 2015 (To appear). [pdf] [slides]
- V. Raman, A. Donzé, D. Sadigh, R. M. Murray, S. A. Seshia, Reactive Synthesis from Signal Temporal Logic Specifications, HSCC 2015 (To appear). [pdf] [slides]
- V. Raman, A. Donzé, M. Maasoumy, R. M. Murray, A. Sangiovanni-Vincentelli, S. A. Seshia, Model Predictive Control with Signal Temporal Logic Specifications, CDC 2014. [pdf] [slides]
- V. Raman, Reactive Switching Protocols for Multi-Robot High-Level Tasks, IROS 2014. [pdf] [slides] [interactive presentation]
- V. Raman, H. Kress-Gazit, Synthesis for Multi-Robot Controllers with Interleaved Motion, ICRA 2014. [pdf] [slides]
- V. Raman, H. Kress-Gazit, Toward Minimal Explanations of Unsynthesizability for High-Level Robot Behaviors, IROS 2013. [pdf] [slides]
- V. Raman, C. Lignos, C. Finucane, M. Marcus, H. Kress-Gazit, Sorry Dave, I'm Afraid I Can't Do That: Explaining Unachievable Robot Tasks Using Natural Language, RSS 2013. [pdf] [slides] [poster]
- V. Raman, N. Piterman, H. Kress-Gazit, Provably Correct Continuous Control for High-Level Robot Behaviors with Actions of Arbitrary Execution Durations, ICRA 2013. [pdf]
- V. Raman, C. Finucane, H. Kress-Gazit, Temporal Logic Robot Mission Planning for Slow and Fast Actions, IROS 2012. [pdf] [slides]
- V. Raman, B. Xu, H. Kress-Gazit, Avoiding Forgetfulness: Structured English Specifications for High-Level Robot Control with Implicit Memory, IROS 2012. [pdf] [slides]
- V. Raman, H. Kress-Gazit, Automated feedback for unachievable high-level robot behaviors, ICRA 2012. [pdf] | [slides] [video]
- V. Raman, H. Kress-Gazit, Analyzing Unsynthesizable Specifications for High-Level Robot Behavior Using LTLMoP, CAV 2011. [pdf] [slides]
- J. Halpern, R. Pass, V. Raman, An Epistemic Characterization of Zero Knowledge, TARK 2009. [pdf] [slides] [poster]
- V. Raman, A. Donzé, M. Maasoumy, Model Predictive Control from Signal Temporal Logic Specifications: A Case Study (Work in Progress), CyPhy 2014. [pdf] [slides]
- R, Ehlers, V. Raman, Low-effort Specification Debugging and Analysis, SYNT 2014. [pdf]
Teaching and Advising
I enjoy teaching and mentoring undergraduates, and have actively sought out relevant opportunities throughout college and graduate school.
- Caltech Undergraduate Student Project Advisor (Fall 2013-present)
- CURIE Academy Teaching Assistant (July 2012)
- Cornell University Autonomous Systems Lab Student Project Advisor (Fall 2011)
- Cornell Computer Science Teaching Assistant: [CS 2110][CS 5846]
- Wellesley College Pforzheimer Learning and Teaching Center Tutor(2004-07)
- Caltech Women Mentoring Women Program, Cornell SWE Mentor, Cornell CSGO-ACSU Mentor
I was Conference Co-Chair and Fundraising Chair for the 2013 Cornell Expanding Your Horizons Conference. EYH aims to stimulate the interest of young girls in math and science, provide them with female scientist role models, and foster awareness of math and science career opportunities. This is a cause dear to me, and I have been involved since my first year in grad school, in a number of capacities.
In the summer of 2011, I ran a communication skills summer course at the MacCormick Secure Center in Brooktondale, NY. MacCormick is a maximum security correctional facility for young men aged 16-21 who have committed violent crimes. Topics covered included techniques for thought organization, and job interview preparation. We worked primarily with young men close to being released, and focused on preparing them to take full advantage of their employment opportunities.
I was a founding member of the Cornell University Computer Science Graduate Organization, and served as its Social Chair from 2009-2011, coordinating department-wide graduate student social events several times a semester.
I enjoy dancing of all sorts, including several forms of partner dancing. I am also trained in Bharatanatyam, and performed with Cornell Sitara throughout graduate school; our style is best, if somewhat nebulously, described as South Asian fusion.
In college, I was a volunteer and instructor for Girls' Lifetime Empowerment and Awareness Program (LEAP), an education program in the Greater Boston area that blends physical skills with self-reflective activities, to foster safety, self-defense and courage in girls, women and their families.
I also have a somewhat significant history with College Mock Trial.