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
Architecture and Compilers Group,
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):
- Regular Functions: 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 a declarative language, DReX, for string transformations based on these foundations.
If you are curious, a good place to start is: talk slides and
talk video (courtesy ETH Zurich).
You are welcome to try out DReX!
- 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.
We have standardized the computational problem of synthesizing program fragments with both logical and syntactic constraints
as Syntax-Guided Synthesis (note: the next competition of solvers
for syntax-guided synthesis will be held in conjunction with CAV 2015).
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 direct.
Every Spring, I teach
CIS 540: Principles of Embedded Computation
for this program. On this topic, I am writing a textbook
Principles of Cyber-Physical Systems which will
be published by MIT Press (scheduled to appear in March 2015).
When I get a chance, I teach CIS 673: Computer-Aided Verification for PhD students.