My research spans formal methods, cyber-physical systems, programming languages, and logic in computer science.
I am a member of Penn's PRECISE Center and
My current research is focused on three directions:
Here are some selected contributions from my past research (complete list of publications):
- Synthesis for System Design:
I am leading NSF Expeditions in Computer Augmented Program Engineering (ExCAPE)
to develop synthesis tools that can assist expert programmers to discover tricky parts
of the code, and/or help end-users perform simple programming tasks without having to write code.
At Penn, we are developing new programming methodology and synthesis tools for design
of distributed protocols, network controllers, and robotic planners
(see the project NetEgg for scenario-based programming of network policies).
We have standardized the computational problem of synthesizing program fragments with both logical and syntactic constraints
as Syntax-Guided Synthesis and have been organizing an annual competition of solvers.
See recent NSF press release on ExCAPE,
and this talk (April 2018) gives an overview of syntax-guided synthesis.
- Programming Abstractions for Processing Data Streams:
Real-time decision making in emerging IoT applications typically
relies on computing quantitative summaries of large
data streams in an efficient and incremental manner. To simplify
the task of programming the desired logic, we are developing StreamQRE, that
has constructs based on regular expressions and quantitative aggregation iterators.
Our compilation algorithm translates
the high-level query into a streaming algorithm with
precise complexity bounds on per-item processing time and
total memory footprint. We are also developing the theoretical framework of
Quantitative Regular Expressions (QRE), and associated transducer models,
as a robust foundation for associating numerical values with data streams.
Current work focuses on processing of data streams in distributed architectures.
If you are curious, a good place to start is: talk slides (April 2018).
- 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. In research funded by DARPA CASE and Assured Autonomy programs, we
are exploring multiple research directions: How to automatically repair models to ensure resiliency in face of unexpected
situations? How to formally verify closed-loop systems that include a neural-network-based controller? How to
integrate logical specifications in reinforcement learning?
At the undergraduate level, I usually teach
CIS 262: Automata, Computability, and Complexity
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!
To train Masters students in the cross-disciplinary skills required for the emerging area of embedded
and cyber-physical systems, Penn Engineering has started a new program
EMBS that I directed for many years.
Every Spring, I teach
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.
When I get a chance, I teach CIS 673: Computer-Aided Verification for PhD students.
- Current PhD Students:
- Current Postdoctoral Researchers:
- Former members:
- Filip Niksic, Postdoctoral researcher, 2018-20.
- Luan Viet Nguyen, Postdoctoral researcher, 2018-19.
Faculty, Department of Computer Science, University of Dayton.
- Nimit Singhania, PhD Fall 2018 (co-advised with Joe Deviette).
Thesis: Static analysis for GPU program performance (pdf)
- Konstantinos Mamouras, Postdoctoral researcher, 2015-18.
Faculty, Department of Computer Science, Rice University.
- Arjun Radhakrishna, Postdoctoral researcher, 2014-17.
- Mukund Raghothaman, PhD Fall 2016.
Thesis: Regular programming over data streams (pdf)
Faculty, Department of Computer Science, University of Southern California.
- Dana Fisman, ExCAPE Research Scientist, 2013-16.
Faculty, Dept of Computer Science,
Ben Gurion University, Israel.
- Salar Moarref, PhD Summer 2016 (co-advised with Ufuk Topcu).
Thesis: Compositional reactive synthesis for multi-agent systems (pdf)
- Yifei Yuan, PhD Summer 2016, (co-advised with Boon Thau Loo).
Thesis: High-level abstractions for programming network policies (pdf)
Abhishek Udupa, PhD, Spring 2016.
Thesis: Synthesis of distributed protocols from scenarios and specifications (pdf)
PhD, Summer 2015.
Thesis: Programming using Automata and Transducers
Faculty, Dept of Computer Science, University of Wisconsin at Madison.
Christos Stergiou, ExCAPE Postdoctoral Researcher, 2013-15.
Sela Mador-Haim, All-But-Dissertation.
- Ashutosh Trivedi, Postdoctoral researcher, 2010-12.
Faculty, Dept. of Computer Science, University of Colorado at Boulder.
- Jyotirmoy Deshmukh, Postdoctoral researcher (as Computing Innovation Fellow), 2010-2012.
Faculty, Dept of Computer Science, University of Southern California.
- Pavol Cerny, PhD Summer 2009.
Thesis: Software model checking for confidentiality
Faculty, Dept of Computer Science, TU Vienna, Austia.
- Gera Weiss, Postdoctoral researcher, 2006-2009.
Faculty, Dept of Computer Science,
Ben Gurion University, Israel.
- Aditya Kanade, Postdoctoral researcher, 2007-2009.
Faculty, Dept of Computer Science and Automation,
Indian Institute of Science, Bangalore.
- Mikhail Bernadsky, PhD Spring 2008.
Thesis: Symbolic analysis of stochastic discrete event systems
Cox Digital Solutions
- Swarat Chaudhuri, PhD Summer 2007.
Thesis: Logics and algorithms for software analysis
Faculty, Department of Computer Science, University of Texas at Austin.
- Sebastian Burckhardt, PhD Summer 2007 (co-advised with Milo Martin).
Thesis: Memory model sensitive analysis of concurrent data types
Microsoft Research, Redmond.
- Wonhong Nam, PhD Spring 2007.
Thesis: Synthesis and compositional verification using language learning
Faculty, Dept of Internet and Multimedia Engineering, Konkuk University, Korea.
- Michael McDougall, PhD Spring 2005 (co-advised with Carl Gunter).
Thesis: Modeling and analyzing integrated policies
Amazon Web Services.
- Madhusudan Parthasarathy, Postdoctoral researcher, 2001-2004.
Faculty, Dept of Computer Science, University of Illinois, Urbana-Champaign.
- Franjo Ivancic,
PhD, Fall 2003.
Thesis: Modeling and Analysis of Hybrid Systems, Abstract
- 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.
- Supratik Mukhopadhyay, Postdoctoral researcher, 2001-02.
Faculty, Dept of Computer Science, Louisiana State University.
- Thao Dang, Postdoctoral researcher, 2000-2001.
CNRS, Grenoble, France.
PhD, Summer 2001.
Thesis: Hierarchical Reduction and Refinement Checking for Asynchronous Processes, Abstract
Academia Sinica, Taiwan.
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
- Radu Grosu, Postdoctoral researcher, 1998--2000.
Faculty of Informatics, TU Vienna, Austria.
- 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),
Minsu Kang (MS, 2001),
Jason Simas (MS, 2004).