I work mainly at the intersection of software engineering and formal methods. I am especially interested in leveraging rigorous modeling and analysis techniques to design software systems that are safe, secure, and reliable. My current interests include sofware design, requirements, modeling, specification and verification, system safety, security, and cyber-physical systems.
I am always looking for motivated students to join our group! If you are interested in any of these topics, please drop me an e-mail or consider applying to the CMU SE PhD program.
- Designing for robustness: What does it mean for software to be robust against an evolving or misbehaving environment? How do we construct systems that are robust by design? (FSE ‘20, RV ‘20, SEAD ‘20)
- Feature interactions: How do detect and safely manage unanticipated interactions between independently-developed system components? (ASE ‘20, RV ‘18)
- Multi-layer security analysis: How do we reason about and mitigate against security attacks that exploit details across multiple levels of abstraction? (CSF ‘22, CAV ‘19, FSE ‘16, SecDev ‘16)
- Resilience in CPS: Can we identify potential safety failures in complex CPS before they occur? How do we recover from such a failure? (RV ‘20, CDC ‘17)
- Sumon Biswas (postdoc)
- Simon Chu (PhD, w/ David Garlan)
- Ian Dardik (PhD)
- Rômulo Meira Góes (postdoc, w/ Stéphane Lafortune and Stavros Tripakis)
- Parv Kapoor (PhD)
- Yining She (PhD)
- CJ Zhang (PhD, w/ David Garlan)
- 17-445/645: SE for AI-enabled Systems (S22, S21, F20, F19)
- 17-614 & 624: Formal Methods (F22, F21, F20)
- 17-651: Models of Software Systems (F19, F18)
Prior to joining CMU, I spent a year working on connected vehicles at Toyota, and was a postdoctoral scholar on the NSF ExCAPE program with Stéphane Lafortune and Stavros Tripakis. I received a PhD in Computer Science at MIT, working with Daniel Jackson. Before MIT, I studied software engineering at the University of Waterloo, where I spent several wonderful terms as an undergraduate researcher in WatForm.