---

Overview

My research is focused on formal methods for system design, and spans artificial intelligence, cyber-physical systems, distributed systems, logic in computer science, machine learning, and programming languages. I am the Director of ASSET (Center for AI-Enabled Systems: Safe, Explainable, and Trustworthy), and also a member of Penn's PRECISE Center and PL Club.

• General Chair, Federated Logic Conference (FLoC), Lisbon, July 2026!
• Online Publications (DBLP, Google Scholar)
• Recent Talks
• Biography
• Curriculum vitae
• Textbook: Principles of Cyber-Physical Systems, MIT Press, 2015

---

Research

My current research is primarily focused on Trustworthy AI and Safe Autonomy. Autonomous systems increasingly rely on machine learning for making decisions. When such systems are used in safety-critical applications such as driverless cars and medical devices, we need guarantees regarding their safety. This motivates research on integrating logical reasoning in learning algorithms. Representative research directions are:

• How to integrate symbolic representations in learning architectures? NSF CISE Distinguished Lecture (June 2025)
• How to design explainable and trustworthy prediction models for clinical decision making? Sample project: KardiaLM for forecasting of adverse cardiac events
• How to integrate logical specifications in reinforcement learning? Sample publications: Temporal logic in RL: Survey, SPECTRL; AAAI'23 Tutorial slides
• How to formally verify closed-loop systems that include a neural-network-based controller? Sample publications: Verisig, EMSOFT'21; Talk (January 2020)

Here are some selected contributions from my past research (complete list of publications):

• Programming abstractions for stream processing systems: Quantitative Regular Expressions, StreamQRE system, and Synchronization schemas, and a talk (April 2018).
• Syntax-guided program synthesis; see original paper and overview talk (April 2021) developed as part of the NSF Expeditions in Computer Augmented Program Engineering (ExCAPE) project.
• All regular transformations in a single pass: Streaming string transducers (see talk), Streaming tree transducers
• Nested Words (aka visibly pushdown languages) for modeling data with linear-hierarchical structure
• Architecture-aware analysis of concurrent software (see PLDI 2007 paper on CheckFence)
• Automata-theoretic approach for compositional scheduling of embedded control software (representative publication)
• CHARON for modeling and verification of hybrid systems
• Multi-agent systems: Reactive Modules (FMSD 1999 paper), Mocha, Alternating-Time Temporal Logic (JACM 2002 paper)
• Specification, Analysis, and Testing of Scenario-based Requirements.
• Hybrid automata (TCS 1995 paper)
• Real-time temporal logics: TPTL (JACM 1994 paper), TCTL (I&C 1993 paper), MITL (JACM 1996 paper)
• Timed automata (TCS 1994 paper); see blogpost and interview when awarded 2016 Alonzo Church award for outstanding contributions to logic and computation.

---

Teaching

• Spring 2026: CIS 4270/5270 Trustworthy Machine Learning
• Spring 2025: Writing and Speaking in Style
• At the undergraduate level, I teach CIS 2620: Automata, Computability, and Complexity, usually each Fall semester. To help students learn the basic model of deterministic finite automata, we have developed an interactive tool AutomataTutor with novel features for automatically generated feedback and automatic grading. If you are an instructor teaching a course on this topic, please encourage your students to use this tool, and if you want to set up a homework assignment using our tool, send us an email!
• CIS 6730: Computer-Aided Verification. Next offering: Spring 2023.
• To train Masters students in the cross-disciplinary skills required for the emerging area of embedded and cyber-physical systems, Penn Engineering started a new program EMBS that I directed for many years. For many years, I taught CIS 540: Principles of Embedded Computation for this program. On this topic, I have written the textbook Principles of Cyber-Physical Systems which was published by MIT Press in April 2015. There are lots of teaching resources such as exercises, solutions, slides, and projects, available if you want to teach a similar course.

---

Research Group

• Current PhD Students:
  1. Seewon Choi
  2. Phillip Hilliard (co-advised with Zack Ives)
  3. Avishree Khare
  4. Guruprerana Shabadi
  5. Emma Shedden (co-advised with Osbert Bastani)
  6. Alaia Solko-Breslin
  7. Chris Watson (co-advised with Dinesh Jayaraman)
  
  
• Former members:
  1. Anton Xue , PhD Summer 2025 (co-advised with Eric Wong)
     Thesis: Trustworthy Machine Learning: Specification, Verification, and Explanation.
     Postdoctoral researcher, Center for Generative AI, University of Texas, Austin
     
  2. Konstantinos Kallas , PhD Summer 2024
     Thesis: Just-in-time scale-out of Shell programs, correctly.
     Faculty, Department of Computer Science, University of California, Los Angeles.
  3. Aalok Thakkar , PhD Summer 2023 (co-advised with Mayur Naik)
     Thesis: Example-guided synthesis of relational queries.
     Faculty, Department of Computer Science, Ashoka University, India.
  4. Kishor Jothimurugan , PhD Spring 2023.
     Thesis: Specification-guided reinforcement learning.
     Two Sigma.
  5. Suguman Bansal , CRA/NSF Computing Innovations Fellow, 2020-22.
     Faculty, Department of Computer Science, Georgia Institute of Technology.
  6. Caleb Stanford , PhD Summer 2022.
     Thesis: Safe programming over distributed streams.
     Faculty, Department of Computer Science, University of California, Davis.
  7. Lei Shi (co-advised with Boon Thau Loo), PhD Spring 2022.
     Thesis: Practical network programming automation.
     Huawei Research.
  8. Radoslav Ivanov Postdoctoral researcher, 2018-21 (co-advised with Insup Lee and George Pappas).
     Faculty, Department of Computer Science, Rensselaer Polytechnic Institute.
  9. Yuepeng Wang , Postdoctoral researcher, 2020-21 (co-advised with Mayur Naik).
     Faculty, Department of Computer Science, Simon Fraser University, Canada.
  10. Filip Niksic , Postdoctoral researcher, 2018-20.
      Google.
  11. Luan Viet Nguyen , Postdoctoral researcher, 2018-19.
      Faculty, Department of Computer Science, University of Dayton.
  12. Nimit Singhania , PhD Fall 2018 (co-advised with Joe Deviette).
      Thesis: Static analysis for GPU program performance (pdf)
      eBay.
  13. Konstantinos Mamouras , Postdoctoral researcher, 2015-18.
      Faculty, Department of Computer Science, Rice University.
  14. Arjun Radhakrishna , Postdoctoral researcher, 2014-17.
      Microsoft.
  15. Mukund Raghothaman , PhD Fall 2016.
      Thesis: Regular programming over data streams (pdf)
      Faculty, Department of Computer Science, University of Southern California.
  16. Dana Fisman , ExCAPE Research Scientist, 2013-16.
      Faculty, Dept of Computer Science, Ben Gurion University, Israel.
  17. Salar Moarref , PhD Summer 2016 (co-advised with Ufuk Topcu).
      Thesis: Compositional reactive synthesis for multi-agent systems (pdf)
      Uber.
  18. Yifei Yuan , PhD Summer 2016, (co-advised with Boon Thau Loo).
      Thesis: High-level abstractions for programming network policies (pdf)
      Alibaba.
  19. Abhishek Udupa , PhD, Spring 2016.
      Thesis: Synthesis of distributed protocols from scenarios and specifications (pdf)
      Microsoft.
  20. Loris D'Antoni , PhD, Summer 2015.
      Thesis: Programming using Automata and Transducers
      Faculty, Dept of Computer Science, University of California, San Diego
  21. Christos Stergiou , ExCAPE Postdoctoral Researcher, 2013-15.
      Google.
  22. Sela Mador-Haim , All-But-Dissertation.
      Coverity.
  23. Ashutosh Trivedi , Postdoctoral researcher, 2010-12.
      Faculty, Dept. of Computer Science, University of Colorado at Boulder.
  24. Jyotirmoy Deshmukh , Postdoctoral researcher (as Computing Innovation Fellow), 2010-2012.
      Faculty, Dept of Computer Science, University of Southern California.
  25. Pavol Cerny , PhD Summer 2009.
      Thesis: Software model checking for confidentiality
      Faculty, Dept of Computer Science, TU Vienna, Austia.
  26. Gera Weiss , Postdoctoral researcher, 2006-2009.
      Faculty, Dept of Computer Science, Ben Gurion University, Israel.
  27. Aditya Kanade , Postdoctoral researcher, 2007-2009.
      Faculty, Dept of Computer Science and Automation, Indian Institute of Science, Bangalore.
  28. Mikhail Bernadsky , PhD Spring 2008.
      Thesis: Symbolic analysis of stochastic discrete event systems
      Cox Digital Solutions
  29. Swarat Chaudhuri , PhD Summer 2007.
      Thesis: Logics and algorithms for software analysis
      Faculty, Department of Computer Science, University of Texas at Austin.
  30. Sebastian Burckhardt , PhD Summer 2007 (co-advised with Milo Martin).
      Thesis: Memory model sensitive analysis of concurrent data types pdf
      Microsoft Research, Redmond.
  31. Wonhong Nam , PhD Spring 2007.
      Thesis: Synthesis and compositional verification using language learning
      Faculty, Dept of Internet and Multimedia Engineering, Konkuk University, Korea.
  32. Michael McDougall , PhD Spring 2005 (co-advised with Carl Gunter).
      Thesis: Modeling and analyzing integrated policies pdf
      Amazon Web Services.
  33. Madhusudan Parthasarathy , Postdoctoral researcher, 2001-2004.
      Faculty, Dept of Computer Science, University of Illinois, Urbana-Champaign.
  34. Franjo Ivancic , PhD, Fall 2003.
      Thesis: Modeling and Analysis of Hybrid Systems, Abstract
      Google.
  35. Zijiang Yang , PhD, Fall 2003.
      Thesis: Techniques for Reducing the Computational Requirements of Symbolic Reachability Analysis, Abstract
      Faculty, Dept of Computer Science, Western Michigan University.
  36. Supratik Mukhopadhyay , Postdoctoral researcher, 2001-02.
      Faculty, Dept of Computer Science, Louisiana State University.
  37. Thao Dang , Postdoctoral researcher, 2000-2001.
      CNRS, Grenoble, France.
      
  38. Bow-Yaw Wang , PhD, Summer 2001.
      Thesis: Hierarchical Reduction and Refinement Checking for Asynchronous Processes, Abstract
      Academia Sinica, Taiwan.
  39. Salvatore La Torre , PhD, Summer 2001.
      Thesis: Verification of Reactive Systems and Decision Problems in Temporal Logic, Abstract
      Faculty, Dept of Computer Science, University of Salerno, Italy
  40. Radu Grosu , Postdoctoral researcher, 1998--2000.
      Faculty of Informatics, TU Vienna, Austria.
  41. George Pappas , Postdoctoral researcher, 1999--2000.
      Faculty, Dept of Electrical and Systems Engineering, University of Pennsylvania.
  
  
• Master's Stduents: Himyanshu Anand (MS, 2000), Arnabnil Bhattacharjee (MS, 1999), Arun Chandrashekharapuram (MS, 2005), Gunjan Gupta (MS, 2004), Steve Hsu (MS, 2022), Minsu Kang (MS, 2001), Jason Simas (MS, 2004), Shaan Vaidya (MS, 2021).

---