My research spans three subdisciplines in computer science:
theoretical computer science (topics such as automata, logics, concurrency, and models of computation);
formal methods in system design (topics such as computer-aided verification, software analysis, and system synthesis); and
cyber-physical systems (topics such as embedded controllers, real-time systems, and hybrid systems).
I am a member of Penn's PRECISE Center, and I also collaborate with Penn's
PL Club and
Theory Research Group.
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.
- Regular Functions and Quantitative Properties of Data Streams: When should a function mapping strings to strings, or strings to numerical costs, or more generally,
strings/trees/infinite-strings to a set of output values with a given set of operations, be considered regular?
We have proposed a new machine model of cost register automata, a class of write-only programs, to
define such a notion of regularity.
We are developing theoretical foundations for this new class
with a focus on algebraic and logical characterization, and algorithms for transformations and analysis questions.
We have also designed the declarative languages DReX, for string-to-string transformations
and QRE (Quantitative Regular Expressions), for expressive quantitative queries over data streams,
based on this foundation.
If you are curious, a good place to start is: talk slides (CPSWeek, April 2016) and
talk video (ETH Zurich, October 2014).
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)
- Arjun Radhakrishna (post-doctoral researcher)
- Former members:
- 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 and Engineering, Indian Institute of Technology, Bombay.
- Jyotirmoy Deshmukh, Research Associate (as Computing Innovation Fellow), 2010-2012.
Toyota Technical Center.
- 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).