My research spans formal methods, cyber-physical systems, programming languages, automata theory, and logic in computer science.
I am a member of Penn's PRECISE Center and
My current research is focused on two 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.
- 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, quantitative aggregation iterators, and
relational calculus. 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.
If you are curious, a good place to start is: talk slides (CPSWeek, April 2016).
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:
- Kostas Mamouras (post-doctoral researcher)
- Former members:
- Arjun Radhakrishna, Post-doctoral researcher, 2014-17.
- Mukund Raghothaman, PhD Fall 2016.
Thesis: Regular programming over data streams (pdf)
Postdoctoral researcher, Penn.
- 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)
Postdoctoral researcher, Cornell University.
- Yifei Yuan, PhD Summer 2016, (co-advised with Boon Thau Loo).
Thesis: High-level abstractions for programming network policies (pdf)
Postdoctoral researcher, CMU.
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, Research associate, 2010-12.
Faculty, Dept. of Computer Science, University of Colorado at Boulder.
- Jyotirmoy Deshmukh, Research Associate (as Computing Innovation Fellow), 2010-2012.
Faculty, Dept of Computer Science, USC.
- Pavol Cerny, PhD Summer 2009.
Thesis: Software model checking for confidentiality
Faculty, Dept of Electrical, Computer, and Energy Engineering, University of Colorado, Boulder.
- Gera Weiss, Research Associate, 2006-2009.
Faculty, Dept of Computer Science,
Ben Gurion University, Israel.
- Aditya Kanade, Research Associate, 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, Rice University.
- 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
- Madhusudan Parthasarathy, Research Associate, 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, Research Associate, 2001-02.
Faculty, Dept of Computer Science, Louisiana State University.
- Thao Dang, Research Associate, 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, Research Associate, 1998--2000.
Faculty of Informatics, TU Vienna, Austria.
- George Pappas,
Research Associate, 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).