TITLE: 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.