*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Tess Malone, Communications Officer
Summary Sentence: Mukund Raghothaman gives a talk.
Full Summary: No summary paragraph submitted.
Mukund RaghothamanTITLE: Declarative Specifications and Statistical Reasoning for Software Design and Analysis
ABSTRACT:
In recent years, declarative approaches have shown great promise in developing high-quality software: on the one hand, they have been used to automatically verify complex properties of large programs, and on the other hand, to concisely express complex computations without sacrificing performance in domains such as big-data processing.
I will first consider program analysis tools, whose goal is to automatically verify the absence of certain classes of bugs. Because of classical limitations such as undecidability, and practical considerations such as scalability, these tools necessarily make approximations and produce many false alarms, resulting in a diminished user experience. If, however, the analysis is expressed in Datalog, a declarative logic programming language, I will show how we may automatically extract a probabilistic model of alarms, and thereby leverage user feedback to reduce the false alarm rate. We have implemented these ideas in a tool named Bingo and demonstrated that it makes the underlying analysis significantly more effective at finding bugs.
I will then consider the problem of programming data stream processing systems. Such systems are used both for monitoring and control in diverse domains such as networks, medical devices, and cyber-physical systems. In this setting, I will present StreamQRE, a language to hierarchically express complex stream processing programs. StreamQRE is a novel integration of linguistic constructs from relational query languages such as SQL and quantitative extensions of regular expressions. While the declarative nature of StreamQRE relieves the programmer of the burden of explicitly maintaining state, our compilation algorithm can automatically extract a high-performance implementation, and even permits substantial memory savings by automatically invoking approximate query evaluation algorithms.
BIO:
Mukund Raghothaman is a postdoctoral researcher at the University of Pennsylvania. His research spans the areas of programming languages, software verification and program synthesis, with the ultimate goal to help programmers create better software with less effort. He previously obtained a Ph.D. in 2017, also from the University of Pennsylvania, where he developed programming abstractions for data stream processing systems.
