Computer Science and Engineering Announces Two Faculty Hires (with More to Come)

Article Content

2017 is shaping up to be another banner year for hiring faculty in one of the fastest-growing departments on the campus of the University of California San Diego.

Professor Dean Tullsen, Chair of the Computer Science and Engineering (CSE) department, announced the first two hires of the faculty recruiting year. Effective July 1, Nadia Polikarpova and Sicun Gao will become assistant professors in the department.

“The unprecedented demand for computer science does not appear to be relenting any time soon,” noted Tullsen. “It is critical that we continue to attract top teaching and research talent to serve what is now the largest computer-science department in the country, and in coming weeks we hope to announce several other new faculty hires to join professors Polikarpova and Gao as incoming faculty for the 2017-2018 academic year.”

Both Gao and Polikarpova will be making the trek to San Diego from Cambridge, Massachusetts, because both are departing the Computer Science and Artificial Intelligence Lab (CSAIL) at the Massachusetts Institute of Technology (MIT) to join the UC San Diego faculty.

Currently Polikarpova is a postdoctoral researcher at MIT CSAIL, which she joined after completing her Ph.D. in Computer Science at ETH Zurich (Switzerland) in 2014. Earlier she did her undergraduate and Master’s degrees in Applied Mathematics and Informatics at ITMO University in Saint Petersburg, Russia. Her honors to date include two Best Paper awards from the International Symposium on Formal Methods.

Gao, also a postdoc at MIT CSAIL, previously did a postdoc at Carnegie Mellon University (CMU), where he completed his Ph.D. in Logic in 2012. His doctoral thesis earned him an honorable mention for CMU’s School of Computer Science Distinguished Doctoral Dissertation Award. Gao’s other honors have included a silver medal for the Gödel Research Prize Fellowship from the Kurt Gödel Society.

Sicun Gao

Dr. Sicun Gao becomes an Assistant Professor in CSE on July 1.

Dr. Gao develops design automation techniques for complex cyber-physical systems, such as autonomous cars and cardiac pacemakers. His research focus is on automated reasoning systems that enable formal reliability guarantees, which cannot be obtained through traditional design methods in this domain. Specifically, Gao developed a practical tool that implements a new algorithmic framework for verifying and synthesizing cyber-physical system designs.

The tool, called dReal, has been used by more than 20 research groups in academia and industry for widely differing applications. The Toyota Research Institute, for example, used dReal in designing autonomous vehicle technology. “It is extremely difficult to build autonomous cars with safety guarantees,” explained Gao in a seminar this spring as part of the CSE Colloquium Lecture Series. “My research addresses this fundamental difficulty in the cyber-physical domain, using an algorithmic approach that breaks down the barriers between the discrete and the continuous.”

According to Gao, by combining the full power of combinatorial search, numerical optimization and statistical learning, the dReal tool provides “formal reliability guarantees that cannot be obtained through simulation and testing.” In addition to Toyota’s project, dReal is also being used to improve security of critical infrastructure, and the developer of a personalized treatment for psoriasis used dReal ahead of clinical trials slated to begin this year at a hospital in the United Kingdom.

Looking to the future, Gao believes that the quest for design automation for cyber-physical systems can lead to the convergence of two separate worlds in artificial intelligence: symbolic reasoning and statistical learning. As such, said Gao, he wants to “build a powerful automated reasoning engine that is crucial for solving challenging problems in a broad range of engineering domains.”

Nadia Polikarpova

Dr. Nadia Polikarpova joins the CSE faculty as Assistant Professor on July 1.

Nadia Polikarpova is generally in the AI field (like Gao), but her research focus is on program verification, program synthesis and software security. “I am interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software,” explained Polikarpova.

“A promising approach to reducing the cost of high-assurance software is to generate provably correct code automatically from high-level specifications,” she added. “My insight was to bring together the latest advances in program synthesis and program verification to achieve this ambitious goal.”

Case in point: Polikarpova developed Synquid, a program synthesizer that can generate larger and more complex programs than what was previously possible with fully automatic synthesis. Moreover, Synquid always produces formally verified code, while requiring up to eight times less programmer effort relative to developing provably correct code manually using a program verifier.

In her research statement, the incoming professor notes that her long-term goal is to “develop a whole new generation of programming languages, where the developer can directly state their system requirements, be it constraints on input-output behavior, global data invariants, security policies, or resource bounds, and the compiler becomes responsible for putting together executable code that provably satisfies these requirements in every execution of the system.”

Polikarpova sees notable examples where her work on verification techniques for synthesis could be highly beneficial in robotics and AI. “Consider a robot that makes decisions based on data derived from multiple sensors, each with its own trade-off between accuracy and cost,” she said. “Building upon a suitable verification technique, capable of reasoning about uncertainty, we could design a synthesis-aided programming language that takes care of configuring the sensors for each safety-critical action in order to guarantee sufficient confidence in the data while minimizing cost.”

Also on her research horizon, Polikarpova intends to develop what she calls a “programmer’s assistant,” a tool that would suggest completions and corrections to your program as you type, by inferring the necessary correctness criteria from existing code. She proposes to combine three complementary sources of information: to derive the programmers’ likely intent from their own code; to leverage testing code that often accompanies software systems; and finally, to use large code bases to build on existing machine-learning techniques to “bias the search towards ‘more natural’ programs.”

Polikarpova is expected to join the Programming Systems group in CSE, with Gao finding a home in the Embedded Systems and Software group, and perhaps both will want to be affiliated with the Artificial Intelligence group. Polikarpova and Gao also have open positions for graduate students and postdoctoral researchers. The incoming faculty members are also expected to join the Contextual Robotics Institute (led by CSE Prof. Henrik Christensen).