Rajeev Alur Zisman Family Professor and Graduate Group Chair Department of Computer and Information Science University of Pennsylvania 609 Levine 3330 Walnut Street, Philadelphia, PA 19104-6389 email: alur at cis upenn edu phone: +1 (215) 573-7483

Overview

• Online Publications (DBLP, Google Scholar)
• Recent Talks
• Biography
• Curriculum vitae
• Textbook: Principles of Cyber-Physical Systems, MIT Press, 2015

Research

• 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).

• Logic in Learning for 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?

• 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

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.

Research Group

• Current PhD Students:
  • Kishor Jothimurugan
  • Caleb Stanford
• Current Postdoctoral Researchers:
  • Luan Viet Nguyen
  • Filip Niksic
• Former members:
  • Nimit Singhania, PhD Fall 2018 (co-advised with Joe Deviette).
    Thesis: Static analysis for GPU program performance (pdf)
    Google.
  • Kostas Mamouras, Post-doctoral researcher, 2015-18.
    Faculty, Department of Computer Science, Rice University.
  • Arjun Radhakrishna, Post-doctoral researcher, 2014-17.
    Microsoft.
  • 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)
    Intentionet.
  • Abhishek Udupa, PhD, Spring 2016.
    Thesis: Synthesis of distributed protocols from scenarios and specifications (pdf)
    Microsoft.
  • Loris D'Antoni, 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.
    Google.
  • Sela Mador-Haim, All-But-Dissertation.
    Coverity.
  • 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 pdf
    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 pdf
    Grammatech Corp.
  • 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
    Google.
  • 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.
    
  • Bow-Yaw Wang, 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).